let n be 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
let m, k1, k2 be FinSequence of NAT ; ( (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 implies ((IDEA_QE (k2,n)) * (IDEA_PE (k1,n))) . m = m )
assume that
A1:
(2 to_power n) + 1 is prime
and
A2:
len m >= 4
and
A3:
( m . 1 is_expressible_by n & m . 2 is_expressible_by n & m . 3 is_expressible_by n & m . 4 is_expressible_by n )
and
A4:
( 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) )
and
A5:
( k2 . 5 = k1 . 5 & k2 . 6 = k1 . 6 )
; ((IDEA_QE (k2,n)) * (IDEA_PE (k1,n))) . m = m
A6:
( (IDEAoperationB (m,k1,n)) . 2 is_expressible_by n & (IDEAoperationB (m,k1,n)) . 3 is_expressible_by n )
by A2, Th27;
A7:
(IDEAoperationB (m,k1,n)) . 4 is_expressible_by n
by A2, Th27;
A8:
( len (IDEAoperationB (m,k1,n)) >= 4 & (IDEAoperationB (m,k1,n)) . 1 is_expressible_by n )
by A2, Def12, Th27;
dom (IDEA_PE (k1,n)) = MESSAGES
by FUNCT_2:def 1;
then
m in dom (IDEA_PE (k1,n))
by FINSEQ_1:def 11;
then ((IDEA_QE (k2,n)) * (IDEA_PE (k1,n))) . m =
(IDEA_QE (k2,n)) . ((IDEA_PE (k1,n)) . m)
by FUNCT_1:13
.=
(IDEA_QE (k2,n)) . (IDEAoperationA ((IDEAoperationB (m,k1,n)),k1,n))
by Def21
.=
IDEAoperationB ((IDEAoperationA ((IDEAoperationA ((IDEAoperationB (m,k1,n)),k1,n)),k2,n)),k2,n)
by Def22
.=
IDEAoperationB ((IDEAoperationB (m,k1,n)),k2,n)
by A1, A4, A8, A6, A7, Th29
.=
m
by A2, A3, A5, Th31
;
hence
((IDEA_QE (k2,n)) * (IDEA_PE (k1,n))) . m = m
; verum