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

now :: thesis: for q, A being object st q in RAT & A in Class (EQRZM V) holds
f1 . (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;

then for q being Element of F_Rat
for A being Element of Class (EQRZM V) holds f1 . (q,A) = f2 . (q,A) ;
hence f1 = f2 by BINOP_1:2; :: thesis: verum