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 that
A1: x1 = x2 and
A2: y1 = y2 ; :: thesis: x1 - y1 = x2 - y2
- y1 = - y2 by A2, Th4;
hence x1 - y1 = x2 - y2 by A1; :: thesis: verum