let i, j be Element of NAT ; :: thesis: [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], TopSpaceMetr (Euclid (i + j)) are_homeomorphic
consider f being Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) such that
A1: f is being_homeomorphism and
for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj by Lm2;
take f ; :: according to T_0TOPSP:def 1 :: thesis: f is being_homeomorphism
thus f is being_homeomorphism by A1; :: thesis: verum