let I be set ; :: thesis: for F being Group-Family of I
for i being object st i in I holds
F . i is Group
let F be Group-Family of I; :: thesis: for i being object st i in I holds
F . i is Group
let i be object ; :: thesis: ( i in I implies F . i is Group )
assume A1: i in I ; :: thesis: F . i is Group
then ex Fi being non empty Group-like multMagma st Fi = F . i by GROUP_7:def 3;
hence F . i is Group by A1; :: thesis: verum