let I be non empty set ; :: thesis: for F being Group-Family of I
for A, B being Subgroup-Family of F st ( for i being Element of I holds A . i = B . i ) holds
A = B
let F be Group-Family of I; :: thesis: for A, B being Subgroup-Family of F st ( for i being Element of I holds A . i = B . i ) holds
A = B
let A, B be Subgroup-Family of F; :: thesis: ( ( for i being Element of I holds A . i = B . i ) implies A = B )
assume for i being Element of I holds A . i = B . i ; :: thesis: A = B
then for i being object st i in I holds
A . i = B . i ;
hence A = B by PBOOLE:3; :: thesis: verum