theorem Th31: :: IDEA_1:31

for n being non zero Nat
for m, k1, k2 being FinSequence of NAT st len m >= 4 & m . 1 is_expressible_by n & m . 2 is_expressible_by n & m . 3 is_expressible_by n & m . 4 is_expressible_by n & k2 . 5 = k1 . 5 & k2 . 6 = k1 . 6 holds
IDEAoperationB ((IDEAoperationB (m,k1,n)),k2,n) = m