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 ((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)); ( ( 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
S1[A,B,f1 . (A,B)]
and
A16:
for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds
S1[A,B,f2 . (A,B)]
; f1 = f2
now 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 ;
( 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) )
;
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
;
verum end;
hence
f1 = f2
by BINOP_1:1; verum