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

now :: thesis: for n being Element of NAT holds |.(seq ").| . n = (|.seq.| ") . n

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:215
.= 1 / |.(seq . n).| by COMPLEX1:48, COMPLEX1:67
.= |.(seq . n).| " by XCMPLX_1:215
.= (|.seq.| . n) " by VALUED_1:18
.= (|.seq.| ") . n by VALUED_1:10 ; :: thesis: verum

end;

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