let f, f1, f2 be complex-valued Function; :: thesis: ( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f )
thus (f1 / f) + (f2 / f) = (f1 (#) (f ^)) + (f2 / f) by Th31
.= (f1 (#) (f ^)) + (f2 (#) (f ^)) by Th31
.= (f1 + f2) (#) (f ^) by Th10
.= (f1 + f2) / f by Th31 ; :: thesis: (f1 / f) - (f2 / f) = (f1 - f2) / f
thus (f1 / f) - (f2 / f) = (f1 (#) (f ^)) - (f2 / f) by Th31
.= (f1 (#) (f ^)) - (f2 (#) (f ^)) by Th31
.= (f1 - f2) (#) (f ^) by Th14
.= (f1 - f2) / f by Th31 ; :: thesis: verum