take [*(+ (* 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*] & [*(+ (* x1,y1),(opp (* x2,y2))),(+ (* x1,y2),(* x2,y1))*] = [*(+ (* 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*] & [*(+ (* x1,y1),(opp (* x2,y2))),(+ (* x1,y2),(* x2,y1))*] = [*(+ (* x1,y1),(opp (* x2,y2))),(+ (* x1,y2),(* x2,y1))*] ) by A2, A4; :: thesis: verum