reconsider x1 = x, y1 = y as Complex by A1;
take x1 + y1 ; :: thesis: ex x1, y1 being Complex st
( x1 = x & y1 = y & x1 + y1 = x1 + y1 )
thus ex x1, y1 being Complex st
( x1 = x & y1 = y & x1 + y1 = x1 + y1 ) ; :: thesis: verum