for n being non zero Nat
for F being Group-like associative multMagma-Family of Seg n
for x being Element of (product F)
for s, t being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds
s = t