let f, g be complex-valued FinSequence; :: thesis: for c being Complex holds c + (f ^ g) = (c + f) ^ (c + g)
let c be Complex; :: thesis: c + (f ^ g) = (c + f) ^ (c + g)
A1: len (c + (f ^ g)) = len (f ^ g) by CARD_1:def 7;
A2: len (c + f) = len f by CARD_1:def 7;
A3: len (c + g) = len g by CARD_1:def 7;
A4: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
A5: len ((c + f) ^ (c + g)) = (len (c + f)) + (len (c + g)) by FINSEQ_1:22;
hence len (c + (f ^ g)) = len ((c + f) ^ (c + g)) by A2, A3, A4, CARD_1:def 7; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (c + (f ^ g)) or (c + (f ^ g)) . b₁ = ((c + f) ^ (c + g)) . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len (c + (f ^ g)) or (c + (f ^ g)) . k = ((c + f) ^ (c + g)) . k )
assume that
A6: 1 <= k and
A7: k <= len (c + (f ^ g)) ; :: thesis: (c + (f ^ g)) . k = ((c + f) ^ (c + g)) . k
k in dom (c + (f ^ g)) by A6, A7, FINSEQ_3:25;
then A8: (c + (f ^ g)) . k = c + ((f ^ g) . k) by VALUED_1:def 2;

per cases ( k <= len f or k > len f ) ;

suppose A9: k <= len f ; :: thesis: (c + (f ^ g)) . k = ((c + f) ^ (c + g)) . k

then A10: (f ^ g) . k = f . k by A6, FINSEQ_1:64;
k in dom (c + f) by A2, A6, A9, FINSEQ_3:25;
hence (c + (f ^ g)) . k = (c + f) . k by A8, A10, VALUED_1:def 2
.= ((c + f) ^ (c + g)) . k by A2, A6, A9, FINSEQ_1:64 ;
:: thesis: verum

end;

suppose A11: k > len f ; :: thesis: (c + (f ^ g)) . k = ((c + f) ^ (c + g)) . k

then A12: (f ^ g) . k = g . (k - (len f)) by A1, A7, FINSEQ_1:24;
A13: (len f) - (len f) < k - (len f) by A11, XREAL_1:9;
A14: k - (len f) is Nat by A11, NAT_1:21;
then A15: 0 + 1 <= k - (len f) by A13, NAT_1:13;
k - (len f) <= ((len f) + (len g)) - (len f) by A1, A4, A7, XREAL_1:9;
then A16: k - (len f) in dom (c + g) by A14, A15, A3, FINSEQ_3:25;
thus (c + (f ^ g)) . k = (c + g) . (k - (len f)) by A8, A12, A16, VALUED_1:def 2
.= ((c + f) ^ (c + g)) . k by A1, A2, A3, A4, A5, A7, A11, FINSEQ_1:24 ; :: thesis: verum

end;

end;