let f, g be complex-valued FinSequence; :: thesis: (f ^ g) ^2 = (f ^2) ^ (g ^2)
A1: len (f ^2) = len f by Th54;
A2: len (g ^2) = len g by Th54;
dom ((f ^ g) ^2) = dom (f ^ g) by VALUED_1:11
.= Seg ((len f) + (len g)) by FINSEQ_1:def 7
.= dom ((f ^2) ^ (g ^2)) by A1, A2, FINSEQ_1:def 7 ;
hence len ((f ^ g) ^2) = len ((f ^2) ^ (g ^2)) 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) ^2) or ((f ^ g) ^2) . b₁ = ((f ^2) ^ (g ^2)) . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len ((f ^ g) ^2) or ((f ^ g) ^2) . k = ((f ^2) ^ (g ^2)) . k )
assume that
A3: 1 <= k and
A4: k <= len ((f ^ g) ^2) ; :: thesis: ((f ^ g) ^2) . k = ((f ^2) ^ (g ^2)) . k
A5: ((f ^ g) ^2) . k = ((f ^ g) . k) ^2 by VALUED_1:11;

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

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

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

end;

suppose A7: k > len f ; :: thesis: ((f ^ g) ^2) . k = ((f ^2) ^ (g ^2)) . 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) ^2) = len (f ^ g) by Th54;
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 ^2) ^ (g ^2)) . k = (g ^2) . i by A1, A2, A10, A11, A12, FINSEQ_1:65;
hence ((f ^ g) ^2) . k = ((f ^2) ^ (g ^2)) . k by A5, A13, VALUED_1:11; :: thesis: verum

end;

end;