let f, g be FinSequence-yielding complex-functions-valued FinSequence; :: thesis: Sum (f ^ g) = (Sum f) ^ (Sum g)
A1: ( len (Sum f) = len f & len (Sum g) = len g & len (Sum (f ^ g)) = len (f ^ g) ) by CARD_1:def 7;
A2: ( len (f ^ g) = (len f) + (len g) & len ((Sum f) ^ (Sum g)) = (len f) + (len g) ) by CARD_1:def 7, FINSEQ_1:22;
A3: ( dom f = dom (Sum f) & dom g = dom (Sum g) ) by Def8;
for i being Nat st 1 <= i & i <= (len f) + (len g) holds
(Sum (f ^ g)) . i = ((Sum f) ^ (Sum g)) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= (len f) + (len g) implies (Sum (f ^ g)) . i = ((Sum f) ^ (Sum g)) . i )
assume A4: ( 1 <= i & i <= (len f) + (len g) ) ; :: thesis: (Sum (f ^ g)) . i = ((Sum f) ^ (Sum g)) . i
A5: ( (Sum (f ^ g)) . i = Sum ((f ^ g) . i) & (Sum f) . i = Sum (f . i) ) by Def8;
A6: i in dom (f ^ g) by A4, A2, FINSEQ_3:25;

per cases ( i in dom f or ex j being Nat st
( j in dom g & i = (len f) + j ) ) by A6, FINSEQ_1:25;

suppose i in dom f ; :: thesis: (Sum (f ^ g)) . i = ((Sum f) ^ (Sum g)) . i

then ( (f ^ g) . i = f . i & ((Sum f) ^ (Sum g)) . i = (Sum f) . i ) by A3, FINSEQ_1:def 7;
hence (Sum (f ^ g)) . i = ((Sum f) ^ (Sum g)) . i by A5; :: thesis: verum

end;

suppose ex j being Nat st
( j in dom g & i = (len f) + j ) ; :: thesis: (Sum (f ^ g)) . i = ((Sum f) ^ (Sum g)) . i

then consider j being Nat such that
A7: ( j in dom g & i = (len f) + j ) ;
( (f ^ g) . i = g . j & ((Sum f) ^ (Sum g)) . i = (Sum g) . j ) by A7, A3, A1, FINSEQ_1:def 7;
hence (Sum (f ^ g)) . i = ((Sum f) ^ (Sum g)) . i by A5, Def8; :: thesis: verum

end;

end;

end;

hence Sum (f ^ g) = (Sum f) ^ (Sum g) by A1, A2; :: thesis: verum