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:217
.= 1 / (abs (seq . n)) by ABSVALUE:15
.= (abs (seq . n)) " by XCMPLX_1:217
.= ((abs seq) . n) " by Th16
.= ((abs seq) " ) . n by VALUED_1:10 ; :: thesis: verum

end;

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