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

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

hence
|.seq.| " = |.(seq ").|
by FUNCT_2:63; :: thesis: verumlet 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;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