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)); ( ( 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)])
; ( 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)])
; f1 = f2
now 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 ;
( 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) )
;
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
;
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; verum