let x1, y1 be Element of F_Complex ; :: thesis: for x2, y2 being complex number st x1 = x2 & y1 = y2 holds
x1 - y1 = x2 - y2
let x2, y2 be complex number ; :: thesis: ( x1 = x2 & y1 = y2 implies x1 - y1 = x2 - y2 )
assume A1: ( x1 = x2 & y1 = y2 ) ; :: thesis: x1 - y1 = x2 - y2
then - y1 = - y2 by Th4;
hence x1 - y1 = x2 - y2 by A1; :: thesis: verum