let g1, g2 be Function of (S ~ A),B; ( ( for x being object st x in the carrier of (S ~ A) holds
ex a, s being Element of A st
( s in S & x = Class ((EqRel S),[a,s]) & g1 . x = (f . a) * ((f . s) ["]) ) ) & ( for x being object st x in the carrier of (S ~ A) holds
ex a, s being Element of A st
( s in S & x = Class ((EqRel S),[a,s]) & g2 . x = (f . a) * ((f . s) ["]) ) ) implies g1 = g2 )
assume that
A7:
for x being object st x in the carrier of (S ~ A) holds
ex a1, s1 being Element of A st
( s1 in S & x = Class ((EqRel S),[a1,s1]) & g1 . x = (f . a1) * ((f . s1) ["]) )
and
A8:
for x being object st x in the carrier of (S ~ A) holds
ex a2, s2 being Element of A st
( s2 in S & x = Class ((EqRel S),[a2,s2]) & g2 . x = (f . a2) * ((f . s2) ["]) )
; g1 = g2
A9: dom g1 =
the carrier of (S ~ A)
by FUNCT_2:def 1
.=
dom g2
by FUNCT_2:def 1
;
now for x being object st x in dom g1 holds
g1 . x = g2 . xlet x be
object ;
( x in dom g1 implies g1 . x = g2 . x )assume A10:
x in dom g1
;
g1 . x = g2 . xthen consider a1,
s1 being
Element of
A such that A11:
s1 in S
and A12:
x = Class (
(EqRel S),
[a1,s1])
and A13:
g1 . x = (f . a1) * ((f . s1) ["])
by A7;
consider a2,
s2 being
Element of
A such that A14:
s2 in S
and A15:
x = Class (
(EqRel S),
[a2,s2])
and A16:
g2 . x = (f . a2) * ((f . s2) ["])
by A8, A10;
reconsider as1 =
[a1,s1] as
Element of
Frac S by A11, Def3;
reconsider as2 =
[a2,s2] as
Element of
Frac S by A14, Def3;
as1,
as2 Fr_Eq S
by A15, A12, Th26;
then consider s3 being
Element of
A such that A18:
s3 in S
and A19:
(((as1 `1) * (as2 `2)) - ((as2 `1) * (as1 `2))) * s3 = 0. A
;
A20:
f is
multiplicative
by A1;
A21:
0. B =
f . (0. A)
by A1, QUOFIELD:50
.=
(f . ((a1 * s2) - (a2 * s1))) * (f . s3)
by A19, A20
;
f . s3 is
Unit of
B
by A1, Th56, A18;
then A22:
f . s3 in Unit_Set B
;
A23:
0. B =
((f . ((a1 * s2) - (a2 * s1))) * (f . s3)) * ((f . s3) ["])
by A21
.=
(f . ((a1 * s2) - (a2 * s1))) * ((f . s3) * ((f . s3) ["]))
by GROUP_1:def 3
.=
(f . ((a1 * s2) - (a2 * s1))) * (1. B)
by A22, Def2
.=
(f . (a1 * s2)) - (f . (a2 * s1))
by A1, RING_2:8
;
f . s1 is
Unit of
B
by A1, A11, Th56;
then A24:
f . s1 in Unit_Set B
;
f . s2 is
Unit of
B
by A1, A14, Th56;
then A26:
f . s2 in Unit_Set B
;
reconsider fa1 =
f . a1,
fa2 =
f . a2 as
Element of
B ;
reconsider fs1 =
f . s1,
fs2 =
f . s2 as
Element of
B ;
A27:
(f . a1) * (f . s2) =
f . (a1 * s2)
by A20
.=
f . (a2 * s1)
by A23, VECTSP_1:27
.=
(f . a2) * (f . s1)
by A20
;
(fa1 * fs2) * (fs2 ["]) =
fa1 * (fs2 * (fs2 ["]))
by GROUP_1:def 3
.=
fa1 * (1. B)
by Def2, A26
.=
fa1
;
then g1 . x =
((fa2 * (fs2 ["])) * fs1) * (fs1 ["])
by A27, A13, GROUP_1:def 3
.=
(fa2 * (fs2 ["])) * (fs1 * (fs1 ["]))
by GROUP_1:def 3
.=
(fa2 * (fs2 ["])) * (1. B)
by A24, Def2
.=
g2 . x
by A16
;
hence
g1 . x = g2 . x
;
verum end;
hence
g1 = g2
by A9; verum