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

proof

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

end;

consider h being Function of (Hom (R,M,N)),(Hom (R,M1,N)) 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,M1,N)) ;
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 = f1 * u )
let f be Element of (Hom (R,M,N)); :: thesis: ex f1 being Homomorphism of R,M,N st
( f = f1 & h . f = f1 * u )
thus ex f1 being Homomorphism of R,M,N st
( f = f1 & h . f = f1 * u ) by A2; :: thesis: verum