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