theorem Th30: :: IDEA_1:30

for n being non zero Nat
for m, k1, k2 being FinSequence of NAT st (2 to_power n) + 1 is prime & 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 & k1 . 1 is_expressible_by n & k1 . 2 is_expressible_by n & k1 . 3 is_expressible_by n & k1 . 4 is_expressible_by n & k2 . 1 = INV_MOD ((k1 . 1),n) & k2 . 2 = NEG_MOD ((k1 . 3),n) & k2 . 3 = NEG_MOD ((k1 . 2),n) & k2 . 4 = INV_MOD ((k1 . 4),n) holds
IDEAoperationA ((IDEAoperationC (IDEAoperationA ((IDEAoperationC m),k1,n))),k2,n) = m