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:93;
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:93;
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;