take T = TopSpaceMetr (Euclid 1); :: thesis: ( T is constituted-FinSeqs & not T is empty & T is strict )
thus for a being Element of T holds a is FinSequence :: according to MONOID_0:def 2 :: thesis: ( not T is empty & T is strict )
proof
let a be Element of T; :: thesis: a is FinSequence
T = TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) by EUCLID:def 8;
hence a is FinSequence ; :: thesis: verum
end;
thus ( not T is empty & T is strict ) ; :: thesis: verum