theorem :: GROUP_23:55

for I being non empty set
for F being Group-Family of I
for G being strict Subgroup of product F
for S being Subgroup-Family of F st ( for i being Element of I holds S . i = Image ((proj (F,i)) * (incl G)) ) holds
for f being Homomorphism-Family of G,S st ( for i being Element of I holds f . i = (proj (F,i)) * (incl G) ) holds
product f = id the carrier of G