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