theorem :: TOPREAL7:26

for i, j being Element of NAT ex f being Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) st
( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj ) ) by Lm2;