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 & i2 <> 0 & $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);

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

S_{1}[A,B,f . (A,B)]
from BINOP_1:sch 1(A1);

reconsider f = f as BinOp of (Class (EQRZM V)) ;

take f ; :: 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

f . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)])

thus 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

f . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) by A14; :: thesis: verum

for i1, i2 being Element of INT.Ring st i1 <> 0 & i2 <> 0 & $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);

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

ex z being object st

( z in Class (EQRZM V) & S_{1}[A,B,z] )

consider f being Function of [:(Class (EQRZM V)),(Class (EQRZM V)):],(Class (EQRZM V)) such that ex z being object st

( z in Class (EQRZM V) & S

let A, B be object ; :: thesis: ( A in Class (EQRZM V) & B in Class (EQRZM V) implies ex z being object st

( z in Class (EQRZM V) & S_{1}[A,B,z] ) )

assume A10: ( A in Class (EQRZM V) & B in Class (EQRZM V) ) ; :: thesis: ex z being object st

( z in Class (EQRZM V) & S_{1}[A,B,z] )

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;

reconsider i1 = i1 as Element of INT.Ring by A3;

consider B1 being object such that

A4: ( B1 in [: the carrier of V,(INT \ {0}):] & B = Class ((EQRZM V),B1) ) by A10, 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 i2 = i2 as Element of INT.Ring by A5;

A61: not i1 * i2 in {0} by A31, A51, TARSKI:def 1;

i1 * i2 in INT \ {0} by XBOOLE_0:def 5, A61;

then X1: [((i2 * z1) + (i1 * z2)),(i1 * i2)] in [: the carrier of V,(INT \ {0}):] by ZFMISC_1:87;

set z = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]);

A7: Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) in Class (EQRZM V) by X1, EQREL_1:def 3;

S_{1}[A,B, Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)])]

( z in Class (EQRZM V) & S_{1}[A,B,z] )
by A7; :: thesis: verum

end;( z in Class (EQRZM V) & S

assume A10: ( A in Class (EQRZM V) & B in Class (EQRZM V) ) ; :: thesis: ex z being object st

( z in Class (EQRZM V) & S

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;

reconsider i1 = i1 as Element of INT.Ring by A3;

consider B1 being object such that

A4: ( B1 in [: the carrier of V,(INT \ {0}):] & B = Class ((EQRZM V),B1) ) by A10, 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 i2 = i2 as Element of INT.Ring by A5;

A61: not i1 * i2 in {0} by A31, A51, TARSKI:def 1;

i1 * i2 in INT \ {0} by XBOOLE_0:def 5, A61;

then X1: [((i2 * z1) + (i1 * z2)),(i1 * i2)] in [: the carrier of V,(INT \ {0}):] by ZFMISC_1:87;

set z = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]);

A7: Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) in Class (EQRZM V) by X1, EQREL_1:def 3;

S

proof

hence
ex z being object st
let zz1, zz2 be Element of V; :: thesis: for i1, i2 being Element of INT.Ring st i1 <> 0 & i2 <> 0 & A = Class ((EQRZM V),[zz1,i1]) & B = Class ((EQRZM V),[zz2,i2]) holds

Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((EQRZM V),[((i2 * zz1) + (i1 * zz2)),(i1 * i2)])

let ii1, ii2 be Element of INT.Ring; :: thesis: ( ii1 <> 0 & ii2 <> 0 & A = Class ((EQRZM V),[zz1,ii1]) & B = Class ((EQRZM V),[zz2,ii2]) implies Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((EQRZM V),[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)]) )

assume A71: ( ii1 <> 0 & ii2 <> 0 & A = Class ((EQRZM V),[zz1,ii1]) & B = Class ((EQRZM V),[zz2,ii2]) ) ; :: thesis: Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((EQRZM V),[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)])

then A72: not ii1 in {0} by TARSKI:def 1;

ii1 in INT \ {0} by XBOOLE_0:def 5, A72;

then X2: [zz1,ii1] in [: the carrier of V,(INT \ {0}):] by ZFMISC_1:87;

X21: not ii2 in {0} by TARSKI:def 1, A71;

ii2 in INT \ {0} by XBOOLE_0:def 5, X21;

then X3: [zz2,ii2] in [: the carrier of V,(INT \ {0}):] by ZFMISC_1:87;

X5: [[zz1,ii1],[z1,i1]] in EQRZM V by X2, A2, A3, A71, EQREL_1:35;

then XX5: ( ii1 <> 0 & i1 <> 0 & i1 * zz1 = ii1 * z1 ) by LMEQR001, AS;

X7: [[zz2,ii2],[z2,i2]] in EQRZM V by X3, A4, A5, A71, EQREL_1:35;

then XX7: ( ii2 <> 0 & i2 <> 0 & i2 * zz2 = ii2 * z2 ) by LMEQR001, AS;

(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 AS, X5, LMEQR001

.= ((ii2 * i2) * (i1 * zz1)) + ((ii1 * i1) * (i2 * zz2)) by AS, X7, LMEQR001

.= (((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 XX5, XX7, LMEQR001, AS;

hence Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((EQRZM V),[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)]) by X1, EQREL_1:35; :: thesis: verum

end;Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((EQRZM V),[((i2 * zz1) + (i1 * zz2)),(i1 * i2)])

let ii1, ii2 be Element of INT.Ring; :: thesis: ( ii1 <> 0 & ii2 <> 0 & A = Class ((EQRZM V),[zz1,ii1]) & B = Class ((EQRZM V),[zz2,ii2]) implies Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((EQRZM V),[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)]) )

assume A71: ( ii1 <> 0 & ii2 <> 0 & A = Class ((EQRZM V),[zz1,ii1]) & B = Class ((EQRZM V),[zz2,ii2]) ) ; :: thesis: Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((EQRZM V),[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)])

then A72: not ii1 in {0} by TARSKI:def 1;

ii1 in INT \ {0} by XBOOLE_0:def 5, A72;

then X2: [zz1,ii1] in [: the carrier of V,(INT \ {0}):] by ZFMISC_1:87;

X21: not ii2 in {0} by TARSKI:def 1, A71;

ii2 in INT \ {0} by XBOOLE_0:def 5, X21;

then X3: [zz2,ii2] in [: the carrier of V,(INT \ {0}):] by ZFMISC_1:87;

X5: [[zz1,ii1],[z1,i1]] in EQRZM V by X2, A2, A3, A71, EQREL_1:35;

then XX5: ( ii1 <> 0 & i1 <> 0 & i1 * zz1 = ii1 * z1 ) by LMEQR001, AS;

X7: [[zz2,ii2],[z2,i2]] in EQRZM V by X3, A4, A5, A71, EQREL_1:35;

then XX7: ( ii2 <> 0 & i2 <> 0 & i2 * zz2 = ii2 * z2 ) by LMEQR001, AS;

(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 AS, X5, LMEQR001

.= ((ii2 * i2) * (i1 * zz1)) + ((ii1 * i1) * (i2 * zz2)) by AS, X7, LMEQR001

.= (((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 XX5, XX7, LMEQR001, AS;

hence Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((EQRZM V),[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)]) by X1, EQREL_1:35; :: thesis: verum

( z in Class (EQRZM V) & S

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

S

reconsider f = f as BinOp of (Class (EQRZM V)) ;

take f ; :: 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

f . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)])

thus 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

f . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) by A14; :: thesis: verum