theorem Th35: :: IDEA_1:35

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 . 2),n) & k2 . 3 = NEG_MOD ((k1 . 3),n) & k2 . 4 = INV_MOD ((k1 . 4),n) & k2 . 5 = k1 . 5 & k2 . 6 = k1 . 6 holds
((IDEA_QE (k2,n)) * (IDEA_PE (k1,n))) . m = m