let X be non empty set ; :: thesis: for f, g being PartFunc of X,COMPLEX holds
( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) )
let f, g be PartFunc of X,COMPLEX ; :: thesis: ( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) )
( Re (f - g) = (Re f) + (Re (- g)) & Im (f - g) = (Im f) + (Im (- g)) ) by COM19;
then ( Re (f - g) = (Re f) + ((- 1) (#) (Re g)) & Im (f - g) = (Im f) + ((- 1) (#) (Im g)) ) by COM21r;
hence ( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) ) ; :: thesis: verum