let f, g be Function of (the Sorts of U1 . s),(OSClass R,s); :: thesis: ( ( for x being Element of the Sorts of U1 . s holds f . x = OSClass R,x ) & ( for x being Element of the Sorts of U1 . s holds g . x = OSClass R,x ) implies f = g )
assume that
A1: for x being Element of the Sorts of U1 . s holds f . x = OSClass R,x and
A2: for x being Element of the Sorts of U1 . s holds g . x = OSClass R,x ; :: thesis: f = g
A3: ( dom f = the Sorts of U1 . s & dom g = the Sorts of U1 . s ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in the Sorts of U1 . s implies f . x = g . x )
assume x in the Sorts of U1 . s ; :: thesis: f . x = g . x
then reconsider x1 = x as Element of the Sorts of U1 . s ;
( f . x = OSClass R,x1 & g . x = OSClass R,x1 ) by A1, A2;
hence f . x = g . x ; :: thesis: verum

end;

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