set cF = the carrier of F_Rat;

set C = Class (EQRZM V);

let f1, f2 be Function of [: the carrier of F_Rat,(Class (EQRZM V)):],(Class (EQRZM V)); :: 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

f1 . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) ) & ( 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

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

assume A7: 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 mm = m & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

f1 . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) ; :: thesis: ( ex q, A being object st

( q in RAT & A in Class (EQRZM V) & ex m, n, i being Integer ex mm being Element of INT.Ring ex z being Element of V st

( m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) & not f2 . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) ) ) or f1 = f2 )

assume A8: 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 mm = m & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

f2 . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) ; :: thesis: f1 = f2

for A being Element of Class (EQRZM V) holds f1 . (q,A) = f2 . (q,A) ;

hence f1 = f2 by BINOP_1:2; :: thesis: verum

set C = Class (EQRZM V);

let f1, f2 be Function of [: the carrier of F_Rat,(Class (EQRZM V)):],(Class (EQRZM V)); :: 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

f1 . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) ) & ( 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

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

assume A7: 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 mm = m & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

f1 . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) ; :: thesis: ( ex q, A being object st

( q in RAT & A in Class (EQRZM V) & ex m, n, i being Integer ex mm being Element of INT.Ring ex z being Element of V st

( m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) & not f2 . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) ) ) or f1 = f2 )

assume A8: 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 mm = m & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds

f2 . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) ; :: thesis: f1 = f2

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

f1 . (q,A) = f2 . (q,A)

then
for q being Element of F_Ratf1 . (q,A) = f2 . (q,A)

let q, A be object ; :: thesis: ( q in RAT & A in Class (EQRZM V) implies f1 . (q,A) = f2 . (q,A) )

assume AS0: ( q in RAT & A in Class (EQRZM V) ) ; :: thesis: f1 . (q,A) = f2 . (q,A)

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 m = m, i = i, n = n as Element of INT.Ring by Lem1;

i <> 0. INT.Ring by A31;

hence f1 . (q,A) = Class ((EQRZM V),[(m * z),(n * i)]) by AS0, A2, A3, A4, A7

.= f2 . (q,A) by AS0, A2, A3, A4, A8, A31 ;

:: thesis: verum

end;assume AS0: ( q in RAT & A in Class (EQRZM V) ) ; :: thesis: f1 . (q,A) = f2 . (q,A)

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 m = m, i = i, n = n as Element of INT.Ring by Lem1;

i <> 0. INT.Ring by A31;

hence f1 . (q,A) = Class ((EQRZM V),[(m * z),(n * i)]) by AS0, A2, A3, A4, A7

.= f2 . (q,A) by AS0, A2, A3, A4, A8, A31 ;

:: thesis: verum

for A being Element of Class (EQRZM V) holds f1 . (q,A) = f2 . (q,A) ;

hence f1 = f2 by BINOP_1:2; :: thesis: verum