let p, q be FinSequence; :: thesis: ( p ^ q is Function-yielding implies ( p is Function-yielding & q is Function-yielding ) )
assume A1: for x being object st x in dom (p ^ q) holds
(p ^ q) . x is Function ; :: according to FUNCOP_1:def 6 :: thesis: ( p is Function-yielding & q is Function-yielding )

hereby :: according to FUNCOP_1:def 6 :: thesis: q is Function-yielding

let x be object ; :: thesis: ( x in dom p implies p . x is Function )
assume A2: x in dom p ; :: thesis: p . x is Function
then (p ^ q) . x = p . x by FINSEQ_1:def 7;
hence p . x is Function by A1, A2, FINSEQ_3:22; :: thesis: verum

end;

let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 q or q . x is set )
assume A3: x in dom q ; :: thesis: q . x is set
then reconsider i = x as Nat ;
(p ^ q) . ((len p) + i) = q . x by A3, FINSEQ_1:def 7;
hence q . x is set by A1, A3, FINSEQ_1:28; :: thesis: verum