let f, g be FinSequence; :: thesis: ( f ^ g is FinSequence-yielding implies ( f is FinSequence-yielding & g is FinSequence-yielding ) )
assume A1: f ^ g is FinSequence-yielding ; :: thesis: ( f is FinSequence-yielding & g is FinSequence-yielding )

A2: now :: thesis: for x being object st x in dom f holds
f . x is FinSequence

let x be object ; :: thesis: ( x in dom f implies f . x is FinSequence )
A3: dom f c= dom (f ^ g) by FINSEQ_1:26;
assume x in dom f ; :: thesis: f . x is FinSequence
then ( f . x = (f ^ g) . x & x in dom (f ^ g) ) by A3, FINSEQ_1:def 7;
hence f . x is FinSequence by A1; :: thesis: verum

end;

now :: thesis: for x being object st x in dom g holds
g . x is FinSequence

let x be object ; :: thesis: ( x in dom g implies g . x is FinSequence )
assume A4: x in dom g ; :: thesis: g . x is FinSequence
then reconsider xx = x as Nat ;
g . x = (f ^ g) . (xx + (len f)) by A4, FINSEQ_1:def 7;
hence g . x is FinSequence by A1; :: thesis: verum

end;

hence ( f is FinSequence-yielding & g is FinSequence-yielding ) by A2, PRE_POLY:def 3; :: thesis: verum