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 Th15
.= (abs G) / (abs H) by Th14 ; :: thesis: verum