let seq be Complex_Sequence; :: thesis: |.seq.| = |.(seq *').|
reconsider rseq1 = |.seq.| as Real_Sequence ;
reconsider rseq2 = |.(seq *').| as Real_Sequence ;
for n being Element of NAT holds |.seq.| . n = |.(seq *').| . n

proof

let n be Element of NAT ; :: thesis: |.seq.| . n = |.(seq *').| . n
|.(seq *').| . n = |.((seq *') . n).| by VALUED_1:18
.= |.((seq . n) *').| by COMSEQ_2:def 2
.= |.(seq . n).| by COMPLEX1:53 ;
hence |.seq.| . n = |.(seq *').| . n by VALUED_1:18; :: thesis: verum

end;

then for n being set st n in NAT holds
rseq1 . n = rseq2 . n ;
hence |.seq.| = |.(seq *').| by FUNCT_2:12; :: thesis: verum