let C be non empty set ; :: thesis: for f, f1, f2 being PartFunc of C,COMPLEX holds
( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f )
let f, f1, f2 be PartFunc of C,COMPLEX; :: 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 Th38
.= (f1 (#) (f ^)) + (f2 (#) (f ^)) by Th38
.= (f1 + f2) (#) (f ^) by Th15
.= (f1 + f2) / f by Th38 ; :: thesis: (f1 / f) - (f2 / f) = (f1 - f2) / f
thus (f1 / f) - (f2 / f) = (f1 (#) (f ^)) - (f2 / f) by Th38
.= (f1 (#) (f ^)) - (f2 (#) (f ^)) by Th38
.= (f1 - f2) (#) (f ^) by Th19
.= (f1 - f2) / f by Th38 ; :: thesis: verum