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

proof

let n be Nat; :: thesis: |.seq.| . n = |.(seq *').| . n
A1: n in NAT by ORDINAL1:def 12;
|.(seq *').| . n = |.((seq *') . n).| by VALUED_1:18
.= |.((seq . n) *').| by COMSEQ_2:def 2, A1
.= |.(seq . n).| by COMPLEX1:53 ;
hence |.seq.| . n = |.(seq *').| . n by VALUED_1:18; :: thesis: verum

end;

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