deffunc H₁( object ) -> Element of K10(( the Sorts of U1 . s)) = Class ((R . s),$1);
consider f being Function such that
A1: ( dom f = the Sorts of U1 . s & ( for x being object st x in the Sorts of U1 . s holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
for x being object st x in the Sorts of U1 . s holds
f . x in (Class R) . s

proof

let x be object ; :: thesis: ( x in the Sorts of U1 . s implies f . x in (Class R) . s )
assume A2: x in the Sorts of U1 . s ; :: thesis: f . x in (Class R) . s
then Class ((R . s),x) in Class (R . s) by EQREL_1:def 3;
then f . x in Class (R . s) by A1, A2;
hence f . x in (Class R) . s by Def6; :: thesis: verum

end;

then reconsider f = f as Function of ( the Sorts of U1 . s),((Class R) . s) by A1, FUNCT_2:3;
take f ; :: thesis: for x being set st x in the Sorts of U1 . s holds
f . x = Class ((R . s),x)
thus for x being set st x in the Sorts of U1 . s holds
f . x = Class ((R . s),x) by A1; :: thesis: verum