theorem Th21: :: POLYNOM3:22

for D1, D2 being set
for f1 being FinSequence of D1 *
for f2 being FinSequence of D2 *
for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 & j1 = j2 )