let x1, y1 be Element of F_Complex; :: thesis: for x2, y2 being Complex st x1 = x2 & y1 = y2 holds
x1 - y1 = x2 - y2
let x2, y2 be Complex; :: 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, Th2;
hence x1 - y1 = x2 - y2 by A1; :: thesis: verum