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