deffunc H₁( Element of S) -> M3( the carrier of S) = x "/\" $1;
thus ex f being Function of S,S st
for x being Element of S holds f . x = H₁(x) from FUNCT_2:sch 4(); :: thesis: verum