scheme :: GROUP_23:sch 4
HomFamSch{ F₁() -> non empty set , F₂() -> Group-Family of F₁(), F₃() -> Group-Family of F₁(), F₄( Element of F₁()) -> Function } :

ex H being Homomorphism-Family of F₂(),F₃() st
for i being Element of F₁() holds H . i = F₄(i)

provided

A1: for i being Element of F₁() holds F₄(i) is Homomorphism of (F₂() . i),(F₃() . i)