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 )
assume A1: ( x1 = x2 & y1 = y2 ) ; :: thesis: addcomplex . x1,y1 = addreal . x2,y2
addcomplex . x1,y1 = x1 + y1 by BINOP_2:def 3;
hence addcomplex . x1,y1 = addreal . x2,y2 by A1, BINOP_2:def 9; :: thesis: verum