:: deftheorem defines /. GROUP_23:def 12 :
for I being non empty set
for F being Group-Family of I
for g being Element of (product F)
for i being Element of I holds g /. i = g . i;