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

now

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

end;

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