let f, g be Function of ((the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o); :: thesis: ( ( for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass R,x ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds g . x = OSClass R,x ) implies f = g )
set SA = the Sorts of A;
set RS = the ResultSort of S;
set rs = the_result_sort_of o;
assume that
A6: for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass R,x and
A7: for x being Element of the Sorts of A . (the_result_sort_of o) holds g . x = OSClass R,x ; :: thesis: f = g
A8: o in the carrier' of S ;
A9: ( dom the ResultSort of S = the carrier' of S & rng the ResultSort of S c= the carrier of S ) by FUNCT_2:def 1;
o in dom (the Sorts of A * the ResultSort of S) by A8, PARTFUN1:def 4;
then A10: (the Sorts of A * the ResultSort of S) . o = the Sorts of A . (the ResultSort of S . o) by FUNCT_1:22
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def 7 ;
dom ((OSClass R) * the ResultSort of S) = dom the ResultSort of S by A9, PARTFUN1:def 4;
then ((OSClass R) * the ResultSort of S) . o = (OSClass R) . (the ResultSort of S . o) by A9, FUNCT_1:22
.= (OSClass R) . (the_result_sort_of o) by MSUALG_1:def 7 ;
then A11: ( dom f = the Sorts of A . (the_result_sort_of o) & rng f c= (OSClass R) . (the_result_sort_of o) & dom g = the Sorts of A . (the_result_sort_of o) & rng g c= (OSClass R) . (the_result_sort_of o) ) by A10, FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in the Sorts of A . (the_result_sort_of o) implies f . x = g . x )
assume x in the Sorts of A . (the_result_sort_of o) ; :: thesis: f . x = g . x
then reconsider x1 = x as Element of the Sorts of A . (the_result_sort_of o) ;
( f . x1 = OSClass R,x1 & g . x1 = OSClass R,x1 ) by A6, A7;
hence f . x = g . x ; :: thesis: verum

end;

hence f = g by A11, FUNCT_1:9; :: thesis: verum