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

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