%0 Journal Article
%T Cartesian Products of Family of Real Linear Spaces
%A Hiroyuki Okazaki
%A Noboru Endou
%A Yasunari Shidama
%J Formalized Mathematics
%@ 1898-9934
%D 2011
%I 
%R 10.2478/v10037-011-0009-2
%X In this article we introduced the isomorphism mapping between cartesian products of family of linear spaces [4]. Those products had been formalized by two different ways, i.e., the way using the functor [:X, Y:] and ones using the functor "product". By the same way, the isomorphism mapping was defined between Cartesian products of family of linear normed spaces also.
%U http://versita.metapress.com/content/e35587t23865134j/?p=25816f9e6d274cf5ab90abc2a2c39abd&pi=8