A2: for G being Group holds F₃(G) is Subgroup of G by A1;
consider S being Subgroup-Family of F₂() such that
A3: for i being Element of F₁() holds S . i = F₃((F₂() . i)) from GROUP_23:sch 2(A2);
for i being Element of F₁() holds S . i is strict Subgroup of F₂() . i

proof

let i be Element of F₁(); :: thesis: S . i is strict Subgroup of F₂() . i
S . i = F₃((F₂() . i)) by A3;
hence S . i is strict Subgroup of F₂() . i by A1; :: thesis: verum

end;

then S is componentwise_strict ;
then reconsider S = S as componentwise_strict Subgroup-Family of F₂() ;
take S ; :: thesis: for i being Element of F₁() holds S . i = F₃((F₂() . i))
thus for i being Element of F₁() holds S . i = F₃((F₂() . i)) by A3; :: thesis: verum