now :: thesis: ( REAL * c= { X where X is FinSequence of REAL : verum } & { X where X is FinSequence of REAL : verum } c= REAL * )

now :: thesis: for x being object st x in REAL * holds
x in { X where X is FinSequence of REAL : verum }

let x be object ; :: thesis: ( x in REAL * implies x in { X where X is FinSequence of REAL : verum } )
assume x in REAL * ; :: thesis: x in { X where X is FinSequence of REAL : verum }
then x is FinSequence of REAL by FINSEQ_1:def 11;
hence x in { X where X is FinSequence of REAL : verum } ; :: thesis: verum

end;

hence REAL * c= { X where X is FinSequence of REAL : verum } ; :: thesis: { X where X is FinSequence of REAL : verum } c= REAL *

now :: thesis: for x being object st x in { X where X is FinSequence of REAL : verum } holds
x in REAL *

let x be object ; :: thesis: ( x in { X where X is FinSequence of REAL : verum } implies x in REAL * )
assume x in { X where X is FinSequence of REAL : verum } ; :: thesis: x in REAL *
then ex X being FinSequence of REAL st x = X ;
hence x in REAL * by FINSEQ_1:def 11; :: thesis: verum

end;

hence { X where X is FinSequence of REAL : verum } c= REAL * ; :: thesis: verum

end;

hence REAL * = { X where X is FinSequence of REAL : verum } ; :: thesis: verum