theorem Th19: :: PENCIL_3:19

for I being non empty finite set
for b1, b2 being ManySortedSet of I
for i being Element of I st b1 . i <> b2 . i holds
diff (b1,b2) = (diff (b1,(b2 +* (i,(b1 . i))))) + 1