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

A2: now :: thesis: for x being object st x in dom f holds
f . x is complex-valued Function

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

end;

now :: thesis: for x being object st x in dom g holds
g . x is complex-valued Function

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

end;

hence ( f is complex-functions-valued & g is complex-functions-valued ) by A2, VALUED_2:def 26; :: thesis: verum