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;