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

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