let n be non empty Element of NAT ; :: thesis: 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 & k1 . 5 is_expressible_by n & k1 . 6 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 & k2 . 5 = k1 . 5 & k2 . 6 = k1 . 6 holds
((IDEA_Q k2,n) * (IDEA_P k1,n)) . m = m
let m, k1, k2 be FinSequence of NAT ; :: thesis: ( (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 & k1 . 5 is_expressible_by n & k1 . 6 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 & k2 . 5 = k1 . 5 & k2 . 6 = k1 . 6 implies ((IDEA_Q k2,n) * (IDEA_P 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 & k1 . 5 is_expressible_by n & k1 . 6 is_expressible_by n ) and
A5: ( 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 ) and
A6: ( k2 . 5 = k1 . 5 & k2 . 6 = k1 . 6 ) ; :: thesis: ((IDEA_Q k2,n) * (IDEA_P k1,n)) . m = m
( dom (IDEA_P k1,n) = MESSAGES & dom (IDEA_Q k2,n) = MESSAGES ) by FUNCT_2:def 1;
then A7: ( m in dom (IDEA_P k1,n) & m in dom (IDEA_Q k2,n) ) by FINSEQ_1:def 11;
A8: len (IDEAoperationB m,k1,n) >= 4 by A2, Def12;
A9: ( (IDEAoperationB m,k1,n) . 1 is_expressible_by n & (IDEAoperationB m,k1,n) . 2 is_expressible_by n & (IDEAoperationB m,k1,n) . 3 is_expressible_by n & (IDEAoperationB m,k1,n) . 4 is_expressible_by n ) by A2, Th28;
((IDEA_Q k2,n) * (IDEA_P k1,n)) . m = (IDEA_Q k2,n) . ((IDEA_P k1,n) . m) by A7, FUNCT_1:23
.= (IDEA_Q k2,n) . (IDEAoperationA (IDEAoperationC (IDEAoperationB m,k1,n)),k1,n) by Def15
.= IDEAoperationB (IDEAoperationA (IDEAoperationC (IDEAoperationA (IDEAoperationC (IDEAoperationB m,k1,n)),k1,n)),k2,n),k2,n by Def16
.= IDEAoperationB (IDEAoperationB m,k1,n),k2,n by A1, A4, A5, A8, A9, Th31
.= m by A1, A2, A3, A4, A6, Th32 ;
hence ((IDEA_Q k2,n) * (IDEA_P k1,n)) . m = m ; :: thesis: verum