defpred S₁[ object , object ] means ex f1 being Homomorphism of R,M,N st
( f1 = $1 & $2 = u * f1 );
A1: for y being Element of (Hom (R,M,N)) ex z being Element of (Hom (R,M,N1)) st S₁[y,z]

proof

let y be Element of (Hom (R,M,N)); :: thesis: ex z being Element of (Hom (R,M,N1)) st S₁[y,z]
reconsider f1 = y as Homomorphism of R,M,N by Lm29;
reconsider uf1 = u * f1 as Homomorphism of R,M,N1 by Th19;
uf1 in set_Hom (M,N1) ;
then reconsider z = uf1 as Element of (Hom (R,M,N1)) ;
S₁[y,z] ;
hence ex z being Element of (Hom (R,M,N1)) st S₁[y,z] ; :: thesis: verum

end;

consider h being Function of (Hom (R,M,N)),(Hom (R,M,N1)) such that
A2: for y being Element of (Hom (R,M,N)) holds S₁[y,h . y] from FUNCT_2:sch 3(A1);
reconsider h = h as Function of (Hom (R,M,N)),(Hom (R,M,N1)) ;
take h ; :: thesis: for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & h . f = u * f1 )
let f be Element of (Hom (R,M,N)); :: thesis: ex f1 being Homomorphism of R,M,N st
( f = f1 & h . f = u * f1 )
thus ex f1 being Homomorphism of R,M,N st
( f = f1 & h . f = u * f1 ) by A2; :: thesis: verum