let D be non empty set ; :: thesis: for G, H being Functional_Sequence of D,REAL holds abs (G / H) = (abs G) / (abs H)
let G, H be Functional_Sequence of D,REAL ; :: thesis: abs (G / H) = (abs G) / (abs H)
thus abs (G / H) = (abs G) (#) (abs (H " )) by Th17
.= (abs G) / (abs H) by Th16 ; :: thesis: verum