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

ex S being componentwise_strict 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 strict Subgroup of G