let seq be Complex_Sequence; :: thesis: |.seq.| " = |.(seq " ).|

now

let n be Element of NAT ; :: thesis: |.(seq " ).| . n = (|.seq.| " ) . n
thus |.(seq " ).| . n = |.((seq " ) . n).| by VALUED_1:18
.= |.((seq . n) " ).| by VALUED_1:10
.= |.(1r / (seq . n)).| by XCMPLX_1:217
.= 1 / |.(seq . n).| by COMPLEX1:134, COMPLEX1:153
.= |.(seq . n).| " by XCMPLX_1:217
.= (|.seq.| . n) " by VALUED_1:18
.= (|.seq.| " ) . n by VALUED_1:10 ; :: thesis: verum

end;

hence |.seq.| " = |.(seq " ).| by FUNCT_2:113; :: thesis: verum