now :: thesis: for x being set st x in dom (p ^ q) holds
(p ^ q) . x is XFinSequence

let x be set ; :: thesis: ( x in dom (p ^ q) implies (p ^ q) . b₁ is XFinSequence )
assume A1: x in dom (p ^ q) ; :: thesis: (p ^ q) . b₁ is XFinSequence
then reconsider x1 = x as Nat ;

per cases ( x1 in dom p or ex l being Nat st
( l in dom q & x1 = (len p) + l ) ) by A1, FINSEQ_1:25;

suppose x1 in dom p ; :: thesis: (p ^ q) . b₁ is XFinSequence

then p . x1 = (p ^ q) . x1 by FINSEQ_1:def 7;
hence (p ^ q) . x is XFinSequence ; :: thesis: verum

end;

suppose ex l being Nat st
( l in dom q & x1 = (len p) + l ) ; :: thesis: (p ^ q) . b₁ is XFinSequence

then consider l being Nat such that
A2: l in dom q and
A3: x = (len p) + l ;
(p ^ q) . ((len p) + l) = q . l by A2, FINSEQ_1:def 7;
hence (p ^ q) . x is XFinSequence by A3; :: thesis: verum

end;

end;

end;

hence p ^ q is XFinSequence-yielding ; :: thesis: verum