let f, g be complex-valued FinSequence; :: thesis: (f ^ g) " = (f ") ^ (g ")
A1: len (f ") = len f by Th55;
A2: len (g ") = len g by Th55;
dom ((f ^ g) ") = dom (f ^ g) by VALUED_1:def 7
.= Seg ((len f) + (len g)) by FINSEQ_1:def 7
.= dom ((f ") ^ (g ")) by A1, A2, FINSEQ_1:def 7 ;
hence len ((f ^ g) ") = len ((f ") ^ (g ")) by FINSEQ_3:29; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len ((f ^ g) ") or ((f ^ g) ") . b₁ = ((f ") ^ (g ")) . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len ((f ^ g) ") or ((f ^ g) ") . k = ((f ") ^ (g ")) . k )
assume that
A3: 1 <= k and
A4: k <= len ((f ^ g) ") ; :: thesis: ((f ^ g) ") . k = ((f ") ^ (g ")) . k
A5: ((f ^ g) ") . k = ((f ^ g) . k) " by VALUED_1:10;

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

suppose A6: k <= len f ; :: thesis: ((f ^ g) ") . k = ((f ") ^ (g ")) . k

hence ((f ^ g) ") . k = (f . k) " by A3, A5, FINSEQ_1:64
.= (f ") . k by VALUED_1:10
.= ((f ") ^ (g ")) . k by A1, A3, A6, FINSEQ_1:64 ;
:: thesis: verum

end;

suppose A7: k > len f ; :: thesis: ((f ^ g) ") . k = ((f ") ^ (g ")) . k

then reconsider i = k - (len f) as Element of NAT by INT_1:5;
A8: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
A9: len ((f ^ g) ") = len (f ^ g) by Th55;
A10: k = (len f) + i ;
A11: 0 + 1 <= k - (len f) by A7, XREAL_1:50, INT_1:7;
A12: k - (len f) <= len g by A4, A8, A9, XREAL_1:20;
then A13: (f ^ g) . k = g . i by A10, A11, FINSEQ_1:65;
((f ") ^ (g ")) . k = (g ") . i by A1, A2, A10, A11, A12, FINSEQ_1:65;
hence ((f ^ g) ") . k = ((f ") ^ (g ")) . k by A5, A13, VALUED_1:10; :: thesis: verum

end;

end;