defpred S1[ object , object , object ] means for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & \$1 = Class ((),[z1,i1]) & \$2 = Class ((),[z2,i2]) holds
\$3 = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]);
set C = Class ();
let f1, f2 be BinOp of (Class ()); :: 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
f1 . (A,B) = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) ) & ( 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
f2 . (A,B) = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) ) implies f1 = f2 )

assume that
A15: for A, B being object st A in Class () & B in Class () holds
S1[A,B,f1 . (A,B)] and
A16: for A, B being object st A in Class () & B in Class () holds
S1[A,B,f2 . (A,B)] ; :: thesis: f1 = f2
now :: thesis: for A, B being set st A in Class () & B in Class () holds
f1 . (A,B) = f2 . (A,B)
let A, B be set ; :: thesis: ( A in Class () & B in Class () implies f1 . (A,B) = f2 . (A,B) )
assume X0: ( A in Class () & B in Class () ) ; :: thesis: f1 . (A,B) = f2 . (A,B)
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;
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 i1 = i1, i2 = i2 as Element of INT.Ring by Lem1;
thus f1 . (A,B) = Class ((),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) by A2, A3, A4, A5, A15, A31, A51, X0
.= f2 . (A,B) by A2, A3, A4, A5, A16, A31, A51, X0 ; :: thesis: verum
end;
hence f1 = f2 by BINOP_1:1; :: thesis: verum