defpred S_{1}[ object , object , object ] means for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st mm = m & n <> 0 & $1 = m / n & i <> 0 & $2 = Class ((EQRZM V),[z,i]) holds

$3 = Class ((EQRZM V),[(mm * z),(n * i)]);

set cF = RAT ;

set C = Class (EQRZM V);

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

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

reconsider f = f as Function of [: the carrier of F_Rat,(Class (EQRZM V)):],(Class (EQRZM V)) ;

take f ; :: thesis: for q, A being object st q in RAT & A in Class (EQRZM V) holds

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

f . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)])

thus for q, A being object st q in RAT & A in Class (EQRZM V) holds

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

f . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) by A14; :: thesis: verum

for mm being Element of INT.Ring

for z being Element of V st mm = m & n <> 0 & $1 = m / n & i <> 0 & $2 = Class ((EQRZM V),[z,i]) holds

$3 = Class ((EQRZM V),[(mm * z),(n * i)]);

set cF = RAT ;

set C = Class (EQRZM V);

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

ex w being object st

( w in Class (EQRZM V) & S_{1}[q,A,w] )

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

( w in Class (EQRZM V) & S

let q, A be object ; :: thesis: ( q in RAT & A in Class (EQRZM V) implies ex w being object st

( w in Class (EQRZM V) & S_{1}[q,A,w] ) )

assume AS0: ( q in RAT & A in Class (EQRZM V) ) ; :: thesis: ex w being object st

( w in Class (EQRZM V) & S_{1}[q,A,w] )

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 z, i being object such that

A3: ( z in the carrier of V & i in INT \ {0} & A1 = [z,i] ) by A2, ZFMISC_1:def 2;

reconsider z = z as Element of V by A3;

( i in INT & not i in {0} ) by XBOOLE_0:def 5, A3;

then A31: ( i in INT & i <> 0 ) by TARSKI:def 1;

reconsider i = i as Integer by A3;

consider m, n being Integer such that

A4: ( n <> 0 & q = m / n ) by AS0, RAT_1:1;

reconsider I = i, mn = m, no = n as Element of INT.Ring by Lem1;

A61: not no * i in {0} by A31, A4, TARSKI:def 1;

no * i in INT by INT_1:def 2;

then no * i in INT \ {0} by XBOOLE_0:def 5, A61;

then X1: [(mn * z),(no * i)] in [: the carrier of V,(INT \ {0}):] by ZFMISC_1:87;

set w = Class ((EQRZM V),[(mn * z),(no * i)]);

A7: Class ((EQRZM V),[(mn * z),(no * i)]) in Class (EQRZM V) by X1, EQREL_1:def 3;

S_{1}[q,A, Class ((EQRZM V),[(mn * z),(no * i)])]

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

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

assume AS0: ( q in RAT & A in Class (EQRZM V) ) ; :: thesis: ex w being object st

( w 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 z, i being object such that

A3: ( z in the carrier of V & i in INT \ {0} & A1 = [z,i] ) by A2, ZFMISC_1:def 2;

reconsider z = z as Element of V by A3;

( i in INT & not i in {0} ) by XBOOLE_0:def 5, A3;

then A31: ( i in INT & i <> 0 ) by TARSKI:def 1;

reconsider i = i as Integer by A3;

consider m, n being Integer such that

A4: ( n <> 0 & q = m / n ) by AS0, RAT_1:1;

reconsider I = i, mn = m, no = n as Element of INT.Ring by Lem1;

A61: not no * i in {0} by A31, A4, TARSKI:def 1;

no * i in INT by INT_1:def 2;

then no * i in INT \ {0} by XBOOLE_0:def 5, A61;

then X1: [(mn * z),(no * i)] in [: the carrier of V,(INT \ {0}):] by ZFMISC_1:87;

set w = Class ((EQRZM V),[(mn * z),(no * i)]);

A7: Class ((EQRZM V),[(mn * z),(no * i)]) in Class (EQRZM V) by X1, EQREL_1:def 3;

S

proof

hence
ex w being object st
let mm, nn, ii be Integer; :: thesis: for mm being Element of INT.Ring

for z being Element of V st mm = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((EQRZM V),[z,ii]) holds

Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(mm * z),(nn * ii)])

let m1 be Element of INT.Ring; :: thesis: for z being Element of V st m1 = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((EQRZM V),[z,ii]) holds

Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(m1 * z),(nn * ii)])

let zz be Element of V; :: thesis: ( m1 = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((EQRZM V),[zz,ii]) implies Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(m1 * zz),(nn * ii)]) )

assume A71: ( m1 = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((EQRZM V),[zz,ii]) ) ; :: thesis: Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(m1 * zz),(nn * ii)])

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

ii in INT by INT_1:def 2;

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

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

reconsider i2 = ii, n1 = nn as Element of INT.Ring by INT_1:def 2;

X51: [[zz,i2],[z,I]] in EQRZM V by X2, A2, A3, A71, EQREL_1:35;

(n1 * i2) * (mn * z) = ((n1 * i2) * mn) * z by VECTSP_1:def 16

.= ((n1 * mn) * i2) * z

.= (n1 * mn) * (i2 * z) by VECTSP_1:def 16

.= (n1 * mn) * (I * zz) by AS, X51, LMEQR001

.= (no * m1) * (I * zz) by A4, A71, XCMPLX_1:95

.= ((no * m1) * I) * zz by VECTSP_1:def 16

.= ((no * I) * m1) * zz

.= (no * I) * (m1 * zz) by VECTSP_1:def 16 ;

then [[(mn * z),(no * I)],[(m1 * zz),(n1 * i2)]] in EQRZM V by A31, A4, A71, LMEQR001, AS;

hence Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(m1 * zz),(nn * ii)]) by X1, EQREL_1:35; :: thesis: verum

end;for z being Element of V st mm = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((EQRZM V),[z,ii]) holds

Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(mm * z),(nn * ii)])

let m1 be Element of INT.Ring; :: thesis: for z being Element of V st m1 = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((EQRZM V),[z,ii]) holds

Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(m1 * z),(nn * ii)])

let zz be Element of V; :: thesis: ( m1 = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((EQRZM V),[zz,ii]) implies Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(m1 * zz),(nn * ii)]) )

assume A71: ( m1 = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((EQRZM V),[zz,ii]) ) ; :: thesis: Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(m1 * zz),(nn * ii)])

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

ii in INT by INT_1:def 2;

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

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

reconsider i2 = ii, n1 = nn as Element of INT.Ring by INT_1:def 2;

X51: [[zz,i2],[z,I]] in EQRZM V by X2, A2, A3, A71, EQREL_1:35;

(n1 * i2) * (mn * z) = ((n1 * i2) * mn) * z by VECTSP_1:def 16

.= ((n1 * mn) * i2) * z

.= (n1 * mn) * (i2 * z) by VECTSP_1:def 16

.= (n1 * mn) * (I * zz) by AS, X51, LMEQR001

.= (no * m1) * (I * zz) by A4, A71, XCMPLX_1:95

.= ((no * m1) * I) * zz by VECTSP_1:def 16

.= ((no * I) * m1) * zz

.= (no * I) * (m1 * zz) by VECTSP_1:def 16 ;

then [[(mn * z),(no * I)],[(m1 * zz),(n1 * i2)]] in EQRZM V by A31, A4, A71, LMEQR001, AS;

hence Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(m1 * zz),(nn * ii)]) by X1, EQREL_1:35; :: thesis: verum

( w in Class (EQRZM V) & S

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

S

reconsider f = f as Function of [: the carrier of F_Rat,(Class (EQRZM V)):],(Class (EQRZM V)) ;

take f ; :: thesis: for q, A being object st q in RAT & A in Class (EQRZM V) holds

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

f . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)])

thus for q, A being object st q in RAT & A in Class (EQRZM V) holds

for m, n, i being Integer

for mm being Element of INT.Ring

for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

f . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) by A14; :: thesis: verum