let c be Complex; :: thesis: <*c*> ^2 = <*(c ^2)*>
A1: len (<*c*> ^2) = len <*c*> by NUMBER15:54
.= 1 by FINSEQ_1:39 ;
hence len (<*c*> ^2) = len <*(c ^2)*> by FINSEQ_1:39; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (<*c*> ^2) or (<*c*> ^2) . b₁ = <*(c ^2)*> . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len (<*c*> ^2) or (<*c*> ^2) . k = <*(c ^2)*> . k )
assume ( 1 <= k & k <= len (<*c*> ^2) ) ; :: thesis: (<*c*> ^2) . k = <*(c ^2)*> . k
then k = 1 by A1, XXREAL_0:1;
hence <*(c ^2)*> . k = (<*c*> . k) ^2
.= (<*c*> ^2) . k by VALUED_1:11 ;
:: thesis: verum