theorem :: GROUP_19:18

for I being non empty set
for F being Group-Family of I
for x being Element of (product F)
for i being Element of I
for g being Element of (F . i) st x = (1_ (product F)) +* (i,g) & g <> 1_ (F . i) holds
support (x,F) = {i}