defpred S_{1}[ 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_{1}[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_{1}[A,B,f2 . (A,B)]
; :: thesis: f1 = f2

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

A16: for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds

S

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)

hence
f1 = f2
by BINOP_1:1; :: thesis: verumf1 . (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;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