let a, b be Element of F_Complex; :: thesis: ( Re (a - b) = (Re a) - (Re b) & Im (a - b) = (Im a) - (Im b) )
reconsider x = a, y = b as Element of COMPLEX by COMPLFLD:def 1;
thus Re (a - b) = Re (x - y) by COMPLFLD:3
.= (Re a) - (Re b) by COMPLEX1:19 ; :: thesis: Im (a - b) = (Im a) - (Im b)
thus Im (a - b) = Im (x - y) by COMPLFLD:3
.= (Im a) - (Im b) by COMPLEX1:19 ; :: thesis: verum