set E = P \/ Q;
consider D being non empty set such that
A1: P \/ Q c= D * by FINSEQ_1:85;
( P c= P \/ Q & Q c= P \/ Q ) by XBOOLE_1:7;
then A3: ( P c= D * & Q c= D * ) by A1;
defpred S₁[ object ] means ex p, q being FinSequence st
( $1 = p ^ q & p in P & q in Q );
consider Y being set such that
A4: for a being object holds
( a in Y iff ( a in D * & S₁[a] ) ) from XBOOLE_0:sch 1();
for a being object st a in Y holds
a is FinSequence

proof

let a be object ; :: thesis: ( a in Y implies a is FinSequence )
assume a in Y ; :: thesis: a is FinSequence
then a in D * by A4;
hence a is FinSequence ; :: thesis: verum

end;

then reconsider Y = Y as FinSequence-membered set by FINSEQ_1:def 19;
take Y ; :: thesis: for a being object holds
( a in Y iff ex p, q being FinSequence st
( a = p ^ q & p in P & q in Q ) )
for a being object holds
( a in Y iff S₁[a] )

proof

let a be object ; :: thesis: ( a in Y iff S₁[a] )
thus ( a in Y implies S₁[a] ) by A4; :: thesis: ( S₁[a] implies a in Y )
assume A5: S₁[a] ; :: thesis: a in Y
then consider p, q being FinSequence such that
A6: a = p ^ q and
A7: p in P and
A8: q in Q ;
reconsider p1 = p as FinSequence of D by A3, A7, FINSEQ_1:def 11;
reconsider q1 = q as FinSequence of D by A3, A8, FINSEQ_1:def 11;
p1 ^ q1 is FinSequence of D ;
then a in D * by A6, FINSEQ_1:def 11;
hence a in Y by A4, A5; :: thesis: verum

end;

hence for a being object holds
( a in Y iff ex p, q being FinSequence st
( a = p ^ q & p in P & q in Q ) ) ; :: thesis: verum