take IT = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*]; :: thesis: ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & IT = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] )
thus ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & IT = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) by A1, A2; :: thesis: verum