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: now :: thesis: for x being object st x in the Sorts of U1 . s holds
f . x = g . x

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

end;

( dom f = the Sorts of U1 . s & dom g = the Sorts of U1 . s ) by FUNCT_2:def 1;
hence f = g by A3, FUNCT_1:2; :: thesis: verum