let f1, f, 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 Th47
.= (f1 (#) (f ^)) + (f2 (#) (f ^)) by Th47
.= (f1 + f2) (#) (f ^) by Th22
.= (f1 + f2) / f by Th47 ; :: thesis: (f1 / f) - (f2 / f) = (f1 - f2) / f
thus (f1 / f) - (f2 / f) = (f1 (#) (f ^)) - (f2 / f) by Th47
.= (f1 (#) (f ^)) - (f2 (#) (f ^)) by Th47
.= (f1 - f2) (#) (f ^) by Th26
.= (f1 - f2) / f by Th47 ; :: thesis: verum