let n be Nat; :: thesis: for f being complex-valued FinSequence holds (f | n) ^2 = (f ^2) | n
let f be complex-valued FinSequence; :: thesis: (f | n) ^2 = (f ^2) | n
A1: len (f ^2) = len f by Th54;

per cases ( n <= len f or len f < n ) ;

suppose A2: n <= len f ; :: thesis: (f | n) ^2 = (f ^2) | n

then A3: len (f | n) = n by FINSEQ_1:59;
dom ((f | n) ^2) = dom (f | n) by VALUED_1:11
.= Seg (len ((f ^2) | n)) by A1, A2, A3, FINSEQ_1:59, FINSEQ_1:def 3
.= dom ((f ^2) | n) by FINSEQ_1:def 3 ;
hence len ((f | n) ^2) = len ((f ^2) | n) by FINSEQ_3:29; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len ((f | n) ^2) or ((f | n) ^2) . b₁ = ((f ^2) | n) . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len ((f | n) ^2) or ((f | n) ^2) . k = ((f ^2) | n) . k )
assume that
1 <= k and
A4: k <= len ((f | n) ^2) ; :: thesis: ((f | n) ^2) . k = ((f ^2) | n) . k
A5: len ((f | n) ^2) = len (f | n) by Th54;
then (f | n) . k = f . k by A3, A4, FINSEQ_3:112;
hence ((f | n) ^2) . k = (f . k) ^2 by VALUED_1:11
.= (f ^2) . k by VALUED_1:11
.= ((f ^2) | n) . k by A3, A4, A5, FINSEQ_3:112 ;
:: thesis: verum

end;

suppose len f < n ; :: thesis: (f | n) ^2 = (f ^2) | n

then ( f | n = f & (f ^2) | n = f ^2 ) by A1, FINSEQ_1:58;
hence (f | n) ^2 = (f ^2) | n ; :: thesis: verum

end;

end;