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