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

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