let X be SubSpace of T; :: thesis: X is constituted-FinSeqs
let p be Element of X; :: according to MONOID_0:def 2 :: thesis: p is set
A1: the carrier of X is Subset of T by TSEP_1:1;
per cases ( not the carrier of X is empty or the carrier of X is empty ) ;
suppose not the carrier of X is empty ; :: thesis: p is set
then p in the carrier of X ;
then reconsider p = p as Point of T by A1;
p is FinSequence ;
hence p is set ; :: thesis: verum
end;
suppose the carrier of X is empty ; :: thesis: p is set
hence p is set ; :: thesis: verum
end;
end;