deffunc H₁( Element of the Sorts of U1 . s) -> Element of OSClass R,s = OSClass R,$1;
thus ex F being Function of (the Sorts of U1 . s),(OSClass R,s) st
for x being Element of the Sorts of U1 . s holds F . x = H₁(x) from FUNCT_2:sch 4(); :: thesis: verum