let g1, g2 be Function of (S ~ A),B; :: thesis: ( ( 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) ["]) ) ; :: thesis: g1 = g2
A9: dom g1 = the carrier of (S ~ A) by FUNCT_2:def 1
.= dom g2 by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom g1 holds
g1 . x = g2 . x

let x be object ; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume A10: x in dom g1 ; :: thesis: g1 . x = g2 . x
then 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 ; :: thesis: verum

end;

hence g1 = g2 by A9; :: thesis: verum