let n be Nat; :: thesis: TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1 )
set J = (Seg n) --> R^1 ;

per cases ( n = 0 or n <> 0 ) ;

suppose A1: n = 0 ; :: thesis: TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1 )

then (Seg n) --> R^1 = {} --> R^1 ;
hence TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1 ) by A1, Lm1; :: thesis: verum

end;

suppose A2: n <> 0 ; :: thesis: TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1 )

A3: REAL n = Funcs (Seg n),REAL by FINSEQ_2:111;
A4: Funcs (Seg n),REAL = product (Carrier ((Seg n) --> R^1 )) by Th25;
then reconsider PP = product_prebasis ((Seg n) --> R^1 ) as Subset-Family of (TopSpaceMetr (Euclid n)) by FINSEQ_2:111;
A5: PP is open by Th27;
PP is quasi_prebasis by A2, Th26;
hence TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1 ) by A4, A3, A5, WAYBEL18:def 3; :: thesis: verum

end;

end;