let x1, y1 be Element of COMPLEX ; :: thesis: for x2, y2 being Real st x1 = x2 & y1 = y2 holds
addcomplex . (x1,y1) = addreal . (x2,y2)
let x2, y2 be Real; :: thesis: ( x1 = x2 & y1 = y2 implies addcomplex . (x1,y1) = addreal . (x2,y2) )
A1: addcomplex . (x1,y1) = x1 + y1 by BINOP_2:def 3;
assume ( x1 = x2 & y1 = y2 ) ; :: thesis: addcomplex . (x1,y1) = addreal . (x2,y2)
hence addcomplex . (x1,y1) = addreal . (x2,y2) by A1, BINOP_2:def 9; :: thesis: verum