let seq9, seq be Real_Sequence; :: thesis: abs (seq9 /" seq) = (abs seq9) /" (abs seq)
thus abs (seq9 /" seq) = (abs seq9) (#) (abs (seq " )) by Th60
.= (abs seq9) /" (abs seq) by Th62 ; :: thesis: verum