defpred S₁[ 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 ((EQRZM V),[z1,i1]) & $2 = Class ((EQRZM V),[z2,i2]) holds
$3 = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]);
set C = Class (EQRZM V);
let f1, f2 be BinOp of (Class (EQRZM V)); :: thesis: ( ( for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) 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 ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds
f1 . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) ) & ( for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) 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 ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds
f2 . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) ) implies f1 = f2 )
assume that
A15: for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds
S₁[A,B,f1 . (A,B)] and
A16: for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds
S₁[A,B,f2 . (A,B)] ; :: thesis: f1 = f2

now :: thesis: for A, B being set st A in Class (EQRZM V) & B in Class (EQRZM V) holds
f1 . (A,B) = f2 . (A,B)

let A, B be set ; :: thesis: ( A in Class (EQRZM V) & B in Class (EQRZM V) implies f1 . (A,B) = f2 . (A,B) )
assume X0: ( A in Class (EQRZM V) & B in Class (EQRZM V) ) ; :: thesis: f1 . (A,B) = f2 . (A,B)
then consider A1 being object such that
A2: ( A1 in [: the carrier of V,(INT \ {0}):] & A = Class ((EQRZM V),A1) ) by EQREL_1:def 3;
consider z1, i1 being object such that
A3: ( z1 in the carrier of V & i1 in INT \ {0} & A1 = [z1,i1] ) by A2, ZFMISC_1:def 2;
reconsider z1 = z1 as Element of V by A3;
( i1 in INT & not i1 in {0} ) by XBOOLE_0:def 5, A3;
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,(INT \ {0}):] & B = Class ((EQRZM V),B1) ) by X0, EQREL_1:def 3;
consider z2, i2 being object such that
A5: ( z2 in the carrier of V & i2 in INT \ {0} & B1 = [z2,i2] ) by A4, ZFMISC_1:def 2;
reconsider z2 = z2 as Element of V by A5;
( i2 in INT & not i2 in {0} ) by XBOOLE_0:def 5, A5;
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 ((EQRZM V),[((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