A2: ex x1, x2, y1, y2 being Element of REAL st
( z = [*x1,x2*] & z9 = [*y1,y2*] & z * z9 = [*(+ (* x1,y1),(opp (* x2,y2))),(+ (* x1,y2),(* x2,y1))*] ) by Def5;
thus z * z9 in COMPLEX by A2; :: according to XCMPLX_0:def 2 :: thesis: verum