for I being non empty set
for G being Group
for x being finite-support Function of I,G
for a being Element of G st I = {1,2} & x = <*a,(1_ G)*> holds
Product x = a