set cF = the carrier of F_Rat;
set C = Class ();
let f1, f2 be Function of [: the carrier of F_Rat,(Class ()):],(Class ()); :: thesis: ( ( for q, A being object st q in RAT & A in Class () 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 ((),[z,i]) holds
f1 . (q,A) = Class ((),[(mm * z),(n * i)]) ) & ( for q, A being object st q in RAT & A in Class () 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 ((),[z,i]) holds
f2 . (q,A) = Class ((),[(mm * z),(n * i)]) ) implies f1 = f2 )

assume A7: for q, A being object st q in RAT & A in Class () 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 ((),[z,i]) holds
f1 . (q,A) = Class ((),[(mm * z),(n * i)]) ; :: thesis: ( ex q, A being object st
( q in RAT & A in Class () & 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 ((),[z,i]) & not f2 . (q,A) = Class ((),[(mm * z),(n * i)]) ) ) or f1 = f2 )

assume A8: for q, A being object st q in RAT & A in Class () 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 ((),[z,i]) holds
f2 . (q,A) = Class ((),[(mm * z),(n * i)]) ; :: thesis: f1 = f2
now :: thesis: for q, A being object st q in RAT & A in Class () holds
f1 . (q,A) = f2 . (q,A)
let q, A be object ; :: thesis: ( q in RAT & A in Class () implies f1 . (q,A) = f2 . (q,A) )
assume AS0: ( q in RAT & A in Class () ) ; :: thesis: f1 . (q,A) = f2 . (q,A)
then consider A1 being object such that
A2: ( A1 in [: the carrier of V,():] & A = Class ((),A1) ) by EQREL_1:def 3;
consider z, i being object such that
A3: ( z in the carrier of V & i in INT \ & A1 = [z,i] ) by ;
reconsider z = z as Element of V by A3;
( i in INT & not i in ) by ;
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 ;
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 ((),[(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 () holds f1 . (q,A) = f2 . (q,A) ;
hence f1 = f2 by BINOP_1:2; :: thesis: verum