deffunc H₁( object ) -> Element of the carrier of S = 1. S;
A: for x being object st x in the carrier of R holds
H₁(x) in the carrier of S ;
ex f being Function of R,S st
for x being object st x in the carrier of R holds
f . x = H₁(x) from FUNCT_2:sch 2(A);
then consider f being Function of R,S such that
H: for x being object st x in the carrier of R holds
f . x = 1. S ;
take f ; :: thesis: f is unity-preserving
thus f is unity-preserving by H; :: thesis: verum