let f, g be Function of (the Sorts of U1 . s),((Class R) . s); :: thesis: ( ( for x being set st x in the Sorts of U1 . s holds
f . x = Class (R . s),x ) & ( for x being set st x in the Sorts of U1 . s holds
g . x = Class (R . s),x ) implies f = g )
assume that
A3: for x being set st x in the Sorts of U1 . s holds
f . x = Class (R . s),x and
A4: for x being set st x in the Sorts of U1 . s holds
g . x = Class (R . s),x ; :: thesis: f = g
A5: ( 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 ( f . x = Class (R . s),x & g . x = Class (R . s),x ) by A3, A4;
hence f . x = g . x ; :: thesis: verum

end;

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