set SA = the Sorts of A;
set RS = the ResultSort of S;
set rs = the_result_sort_of o;
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 )
assume that
A5: for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass (R,x) and
A6: for x being Element of the Sorts of A . (the_result_sort_of o) holds g . x = OSClass (R,x) ; :: thesis: f = g

A7: now :: thesis: for x being object st x in the Sorts of A . (the_result_sort_of o) holds
f . x = g . x

let x be object ; :: 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) by A5;
hence f . x = g . x by A6; :: thesis: verum

end;

o in the carrier' of S ;
then o in dom ( the Sorts of A * the ResultSort of S) by PARTFUN1:def 2;
then ( the Sorts of A * the ResultSort of S) . o = the Sorts of A . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def 2 ;
then ( dom f = the Sorts of A . (the_result_sort_of o) & dom g = the Sorts of A . (the_result_sort_of o) ) by FUNCT_2:def 1;
hence f = g by A7, FUNCT_1:2; :: thesis: verum