scheme :: GROUP_23:sch 2
SubFamSch{ F₁() -> non empty set , F₂() -> Group-Family of F₁(), F₃( Group) -> Group } :

ex S being Subgroup-Family of F₂() st
for i being Element of F₁() holds S . i = F₃((F₂() . i))

provided

A1: for G being Group holds F₃(G) is Subgroup of G