let n be non zero 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 & 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) holds
((IDEA_QS (k2,n)) * (IDEA_PS (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 & 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) implies ((IDEA_QS (k2,n)) * (IDEA_PS (k1,n))) . m = m )
assume A1: ( (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) ) ; :: thesis: ((IDEA_QS (k2,n)) * (IDEA_PS (k1,n))) . m = m
dom (IDEA_PS (k1,n)) = MESSAGES by FUNCT_2:def 1;
then m in dom (IDEA_PS (k1,n)) by FINSEQ_1:def 11;
then ((IDEA_QS (k2,n)) * (IDEA_PS (k1,n))) . m = (IDEA_QS (k2,n)) . ((IDEA_PS (k1,n)) . m) by FUNCT_1:13
.= (IDEA_QS (k2,n)) . (IDEAoperationA (m,k1,n)) by Def19
.= IDEAoperationA ((IDEAoperationA (m,k1,n)),k2,n) by Def20
.= m by A1, Th29 ;
hence ((IDEA_QS (k2,n)) * (IDEA_PS (k1,n))) . m = m ; :: thesis: verum