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:139 ;
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:18; :: thesis: verum