let seq be Real_Sequence; :: thesis: (abs seq) " = abs (seq ")

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

let n be Element of NAT ; :: thesis: (abs (seq ")) . n = ((abs seq) ") . n
thus (abs (seq ")) . n = |.((seq ") . n).| by Th12
.= |.((seq . n) ").| by VALUED_1:10
.= |.(1 / (seq . n)).| by XCMPLX_1:215
.= 1 / |.(seq . n).| by ABSVALUE:7
.= |.(seq . n).| " by XCMPLX_1:215
.= ((abs seq) . n) " by Th12
.= ((abs seq) ") . n by VALUED_1:10 ; :: thesis: verum

end;

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