deffunc H₁( set ) -> Element of K6((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 set st x in the Sorts of U1 . s holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
for x being set st x in the Sorts of U1 . s holds
f . x in (Class R) . s

proof

let x be set ; :: 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 5;
then f . x in Class (R . s) by A1, A2;
hence f . x in (Class R) . s by Def8; :: thesis: verum

end;

then reconsider f = f as Function of (the Sorts of U1 . s),((Class R) . s) by A1, FUNCT_2:5;
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