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)) by Th5;
then A1: Re (f - g) = (Re f) + ((- 1) (#) (Re g)) by Th2;
Im (f - g) = (Im f) + (Im (- g)) by Th5;
hence ( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) ) by A1, Th2; :: thesis: verum