let I be non empty set ; :: thesis: for F being Group-Family of I holds support ((1_ (product F)),F) is empty
let F be Group-Family of I; :: thesis: support ((1_ (product F)),F) is empty
for i being object holds not i in support ((1_ (product F)),F)

proof

let i be object ; :: thesis: not i in support ((1_ (product F)),F)
assume i in support ((1_ (product F)),F) ; :: thesis: contradiction
then ex Z being Group st
( Z = F . i & (1_ (product F)) . i <> 1_ Z & i in I ) by Def1;
hence contradiction by GROUP_7:6; :: thesis: verum

end;

hence support ((1_ (product F)),F) is empty by XBOOLE_0:def 1; :: thesis: verum