let I be non empty set ; :: thesis: for F, S being Group-Family of I holds
( S is Subgroup-Family of F iff for i being Element of I holds S . i is Subgroup of F . i )
let F, S be Group-Family of I; :: thesis: ( S is Subgroup-Family of F iff for i being Element of I holds S . i is Subgroup of F . i )
thus ( S is Subgroup-Family of F implies for i being Element of I holds S . i is Subgroup of F . i ) :: thesis: ( ( for i being Element of I holds S . i is Subgroup of F . i ) implies S is Subgroup-Family of F )

proof

assume A1: S is Subgroup-Family of F ; :: thesis: for i being Element of I holds S . i is Subgroup of F . i
let i be Element of I; :: thesis: S . i is Subgroup of F . i
reconsider SS = S as Subgroup-Family of F by A1;
S . i = SS . i ;
hence S . i is Subgroup of F . i ; :: thesis: verum

end;

assume for i being Element of I holds S . i is Subgroup of F . i ; :: thesis: S is Subgroup-Family of F
then S is F -Subgroup-yielding ;
hence S is Subgroup-Family of F ; :: thesis: verum