defpred S1[ object , object , object ] means for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0 & i2 <> 0 & \$1 = Class ((),[z1,i1]) & \$2 = Class ((),[z2,i2]) holds
\$3 = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]);
set C = Class ();
A1: now :: thesis: for A, B being object st A in Class () & B in Class () holds
ex z being object st
( z in Class () & S1[A,B,z] )
let A, B be object ; :: thesis: ( A in Class () & B in Class () implies ex z being object st
( z in Class () & S1[A,B,z] ) )

assume A10: ( A in Class () & B in Class () ) ; :: thesis: ex z being object st
( z in Class () & S1[A,B,z] )

then consider A1 being object such that
A2: ( A1 in [: the carrier of V,():] & A = Class ((),A1) ) by EQREL_1:def 3;
consider z1, i1 being object such that
A3: ( z1 in the carrier of V & i1 in INT \ & A1 = [z1,i1] ) by ;
reconsider z1 = z1 as Element of V by A3;
( i1 in INT & not i1 in ) by ;
then A31: ( i1 in INT & i1 <> 0 ) by TARSKI:def 1;
reconsider i1 = i1 as Integer by A3;
reconsider i1 = i1 as Element of INT.Ring by A3;
consider B1 being object such that
A4: ( B1 in [: the carrier of V,():] & B = Class ((),B1) ) by ;
consider z2, i2 being object such that
A5: ( z2 in the carrier of V & i2 in INT \ & B1 = [z2,i2] ) by ;
reconsider z2 = z2 as Element of V by A5;
( i2 in INT & not i2 in ) by ;
then A51: ( i2 in INT & i2 <> 0 ) by TARSKI:def 1;
reconsider i2 = i2 as Integer by A5;
reconsider i2 = i2 as Element of INT.Ring by A5;
A61: not i1 * i2 in by ;
i1 * i2 in INT \ by ;
then X1: [((i2 * z1) + (i1 * z2)),(i1 * i2)] in [: the carrier of V,():] by ZFMISC_1:87;
set z = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]);
A7: Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) in Class () by ;
S1[A,B, Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)])]
proof
let zz1, zz2 be Element of V; :: thesis: for i1, i2 being Element of INT.Ring st i1 <> 0 & i2 <> 0 & A = Class ((),[zz1,i1]) & B = Class ((),[zz2,i2]) holds
Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((),[((i2 * zz1) + (i1 * zz2)),(i1 * i2)])

let ii1, ii2 be Element of INT.Ring; :: thesis: ( ii1 <> 0 & ii2 <> 0 & A = Class ((),[zz1,ii1]) & B = Class ((),[zz2,ii2]) implies Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((),[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)]) )
assume A71: ( ii1 <> 0 & ii2 <> 0 & A = Class ((),[zz1,ii1]) & B = Class ((),[zz2,ii2]) ) ; :: thesis: Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((),[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)])
then A72: not ii1 in by TARSKI:def 1;
ii1 in INT \ by ;
then X2: [zz1,ii1] in [: the carrier of V,():] by ZFMISC_1:87;
X21: not ii2 in by ;
ii2 in INT \ by ;
then X3: [zz2,ii2] in [: the carrier of V,():] by ZFMISC_1:87;
X5: [[zz1,ii1],[z1,i1]] in EQRZM V by ;
then XX5: ( ii1 <> 0 & i1 <> 0 & i1 * zz1 = ii1 * z1 ) by ;
X7: [[zz2,ii2],[z2,i2]] in EQRZM V by ;
then XX7: ( ii2 <> 0 & i2 <> 0 & i2 * zz2 = ii2 * z2 ) by ;
(ii1 * ii2) * ((i2 * z1) + (i1 * z2)) = ((ii1 * ii2) * (i2 * z1)) + ((ii1 * ii2) * (i1 * z2)) by VECTSP_1:def 14
.= (((ii1 * ii2) * i2) * z1) + ((ii1 * ii2) * (i1 * z2)) by VECTSP_1:def 16
.= (((ii2 * i2) * ii1) * z1) + (((ii1 * ii2) * i1) * z2) by VECTSP_1:def 16
.= ((ii2 * i2) * (ii1 * z1)) + (((ii1 * i1) * ii2) * z2) by VECTSP_1:def 16
.= ((ii2 * i2) * (ii1 * z1)) + ((ii1 * i1) * (ii2 * z2)) by VECTSP_1:def 16
.= ((ii2 * i2) * (i1 * zz1)) + ((ii1 * i1) * (ii2 * z2)) by
.= ((ii2 * i2) * (i1 * zz1)) + ((ii1 * i1) * (i2 * zz2)) by
.= (((ii2 * i2) * i1) * zz1) + ((ii1 * i1) * (i2 * zz2)) by VECTSP_1:def 16
.= (((i2 * i1) * ii2) * zz1) + (((ii1 * i1) * i2) * zz2) by VECTSP_1:def 16
.= ((i1 * i2) * (ii2 * zz1)) + (((i1 * i2) * ii1) * zz2) by VECTSP_1:def 16
.= ((i1 * i2) * (ii2 * zz1)) + ((i1 * i2) * (ii1 * zz2)) by VECTSP_1:def 16
.= (i1 * i2) * ((ii2 * zz1) + (ii1 * zz2)) by VECTSP_1:def 14 ;
then [[((i2 * z1) + (i1 * z2)),(i1 * i2)],[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)]] in EQRZM V by ;
hence Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((),[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)]) by ; :: thesis: verum
end;
hence ex z being object st
( z in Class () & S1[A,B,z] ) by A7; :: thesis: verum
end;
consider f being Function of [:(Class ()),(Class ()):],(Class ()) such that
A14: for A, B being object st A in Class () & B in Class () holds
S1[A,B,f . (A,B)] from reconsider f = f as BinOp of (Class ()) ;
take f ; :: thesis: for A, B being object st A in Class () & B in Class () holds
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((),[z1,i1]) & B = Class ((),[z2,i2]) holds
f . (A,B) = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)])

thus for A, B being object st A in Class () & B in Class () holds
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((),[z1,i1]) & B = Class ((),[z2,i2]) holds
f . (A,B) = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) by A14; :: thesis: verum