let n be non empty Element of NAT ; :: thesis:
let lk be Element of NAT ; :: thesis:
let Key1, Key2 be Matrix of lk,6, NAT ; :: thesis:
let r be Element of NAT ; :: thesis:
let ks1, ks2, ke1, ke2 be FinSequence of NAT ; :: thesis:
let m be FinSequence of NAT ; :: thesis:
assume that
A1: lk >= r and
A2: (2 to_power n) + 1 is prime and
A3: len m >= 4 and
A4: ( 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
A5: for i being Element of NAT st i <= r holds
( Key1 * i,1 is_expressible_by n & Key1 * i,2 is_expressible_by n & Key1 * i,3 is_expressible_by n & Key1 * i,4 is_expressible_by n & Key1 * i,5 is_expressible_by n & Key1 * i,6 is_expressible_by n & Key2 * i,1 is_expressible_by n & Key2 * i,2 is_expressible_by n & Key2 * i,3 is_expressible_by n & Key2 * i,4 is_expressible_by n & Key2 * i,5 is_expressible_by n & Key2 * i,6 is_expressible_by n & Key2 * i,1 = INV_MOD (Key1 * i,1),n & Key2 * i,2 = NEG_MOD (Key1 * i,3),n & Key2 * i,3 = NEG_MOD (Key1 * i,2),n & Key2 * i,4 = INV_MOD (Key1 * i,4),n & Key1 * i,5 = Key2 * i,5 & Key1 * i,6 = Key2 * i,6 ) and
A6: ( ks1 . 1 is_expressible_by n & ks1 . 2 is_expressible_by n & ks1 . 3 is_expressible_by n & ks1 . 4 is_expressible_by n & ks2 . 1 = INV_MOD (ks1 . 1),n & ks2 . 2 = NEG_MOD (ks1 . 2),n & ks2 . 3 = NEG_MOD (ks1 . 3),n & ks2 . 4 = INV_MOD (ks1 . 4),n ) and
A7: ( ke1 . 1 is_expressible_by n & ke1 . 2 is_expressible_by n & ke1 . 3 is_expressible_by n & ke1 . 4 is_expressible_by n & ke2 . 1 = INV_MOD (ke1 . 1),n & ke2 . 2 = NEG_MOD (ke1 . 2),n & ke2 . 3 = NEG_MOD (ke1 . 3),n & ke2 . 4 = INV_MOD (ke1 . 4),n & ke2 . 5 = ke1 . 5 & ke2 . 6 = ke1 . 6 ) ; :: thesis:
A8: m in MESSAGES by FINSEQ_1:def 11;
then (IDEA_PS ks1,n) . m in MESSAGES by FUNCT_2:7;
then reconsider m1 = (IDEA_PS ks1,n) . m as FinSequence of NAT by FINSEQ_1:def 11;
A9: m1 in MESSAGES by FINSEQ_1:def 11;
A10: len m1 = len (IDEAoperationA m,ks1,n) by Def19
.= len m by Def11 ;
m1 . 4 = (IDEAoperationA m,ks1,n) . 4 by Def19;
then A11: m1 . 4 is_expressible_by n by A3, Th27;
m1 . 3 = (IDEAoperationA m,ks1,n) . 3 by Def19;
then A12: m1 . 3 is_expressible_by n by A3, Th27;
m1 . 2 = (IDEAoperationA m,ks1,n) . 2 by Def19;
then A13: m1 . 2 is_expressible_by n by A3, Th27;
m1 . 1 = (IDEAoperationA m,ks1,n) . 1 by Def19;
then A14: m1 . 1 is_expressible_by n by A3, Th27;

per cases ;

suppose A15: r = 0 ; :: thesis:

then len (IDEA_Q_F Key2,n,r) = 0 by Def18;
then A16: IDEA_Q_F Key2,n,r = {} ;
len (IDEA_P_F Key1,n,r) = 0 by A15, Def17;
then IDEA_P_F Key1,n,r = {} ;
hence ((IDEA_QS ks2,n) * ((compose (IDEA_Q_F Key2,n,r),MESSAGES ) * ((IDEA_QE ke2,n) * ((IDEA_PE ke1,n) * ((compose (IDEA_P_F Key1,n,r),MESSAGES ) * (IDEA_PS ks1,n)))))) . m = ((IDEA_QS ks2,n) * ((compose {} ,MESSAGES ) * ((IDEA_QE ke2,n) * ((IDEA_PE ke1,n) * ((compose {} ,MESSAGES ) * (IDEA_PS ks1,n)))))) . m by A16
.= ((IDEA_QS ks2,n) * ((id MESSAGES ) * ((IDEA_QE ke2,n) * ((IDEA_PE ke1,n) * ((compose {} ,MESSAGES ) * (IDEA_PS ks1,n)))))) . m by FUNCT_7:41
.= ((IDEA_QS ks2,n) * ((id MESSAGES ) * ((IDEA_QE ke2,n) * ((IDEA_PE ke1,n) * ((id MESSAGES ) * (IDEA_PS ks1,n)))))) . m by FUNCT_7:41
.= ((IDEA_QS ks2,n) * ((IDEA_QE ke2,n) * ((IDEA_PE ke1,n) * ((id MESSAGES ) * (IDEA_PS ks1,n))))) . m by FUNCT_2:23
.= ((IDEA_QS ks2,n) * ((IDEA_QE ke2,n) * ((IDEA_PE ke1,n) * (IDEA_PS ks1,n)))) . m by FUNCT_2:23
.= (IDEA_QS ks2,n) . (((IDEA_QE ke2,n) * ((IDEA_PE ke1,n) * (IDEA_PS ks1,n))) . m) by A8, FUNCT_2:21
.= (IDEA_QS ks2,n) . ((IDEA_QE ke2,n) . (((IDEA_PE ke1,n) * (IDEA_PS ks1,n)) . m)) by A8, FUNCT_2:21
.= (IDEA_QS ks2,n) . ((IDEA_QE ke2,n) . ((IDEA_PE ke1,n) . m1)) by A8, FUNCT_2:21
.= (IDEA_QS ks2,n) . (((IDEA_QE ke2,n) * (IDEA_PE ke1,n)) . m1) by A9, FUNCT_2:21
.= (IDEA_QS ks2,n) . ((IDEA_PS ks1,n) . m) by A2, A3, A7, A10, A14, A13, A12, A11, Th36
.= ((IDEA_QS ks2,n) * (IDEA_PS ks1,n)) . m by A8, FUNCT_2:21
.= m by A2, A3, A4, A6, Th35 ;
:: thesis:

end;

suppose A17: r <> 0 ; :: thesis:

then A18: IDEA_P_F Key1,n,r is FuncSequence of MESSAGES , MESSAGES by Th41;
then A19: firstdom (IDEA_P_F Key1,n,r) = MESSAGES by FUNCT_7:def 9;
then A20: dom (compose (IDEA_P_F Key1,n,r),MESSAGES ) = MESSAGES by A18, FUNCT_7:64;
( IDEA_P_F Key1,n,r = {} implies rng (compose (IDEA_P_F Key1,n,r),MESSAGES ) = {} ) by A19, FUNCT_7:def 6;
then A21: rng (compose (IDEA_P_F Key1,n,r),MESSAGES ) c= lastrng (IDEA_P_F Key1,n,r) by FUNCT_7:61, XBOOLE_1:2;
lastrng (IDEA_P_F Key1,n,r) c= MESSAGES by A18, FUNCT_7:def 9;
then rng (compose (IDEA_P_F Key1,n,r),MESSAGES ) c= MESSAGES by A21, XBOOLE_1:1;
then reconsider PF = compose (IDEA_P_F Key1,n,r),MESSAGES as Function of MESSAGES ,MESSAGES by A20, FUNCT_2:def 1, RELSET_1:11;
A22: rng PF c= MESSAGES by RELAT_1:def 19;
PF . m1 in MESSAGES by A9, FUNCT_2:7;
then reconsider m2 = PF . m1 as FinSequence of NAT by FINSEQ_1:def 11;
A23: ( len m2 >= 4 & m2 . 1 is_expressible_by n ) by A3, A10, A14, A13, A12, A11, Th47;
A24: IDEA_Q_F Key2,n,r is FuncSequence of MESSAGES , MESSAGES by A17, Th42;
then A25: firstdom (IDEA_Q_F Key2,n,r) = MESSAGES by FUNCT_7:def 9;
then A26: dom (compose (IDEA_Q_F Key2,n,r),MESSAGES ) = MESSAGES by A24, FUNCT_7:64;
( IDEA_Q_F Key2,n,r = {} implies rng (compose (IDEA_Q_F Key2,n,r),MESSAGES ) = {} ) by A25, FUNCT_7:def 6;
then A27: rng (compose (IDEA_Q_F Key2,n,r),MESSAGES ) c= lastrng (IDEA_Q_F Key2,n,r) by FUNCT_7:61, XBOOLE_1:2;
lastrng (IDEA_Q_F Key2,n,r) c= MESSAGES by A24, FUNCT_7:def 9;
then rng (compose (IDEA_Q_F Key2,n,r),MESSAGES ) c= MESSAGES by A27, XBOOLE_1:1;
then reconsider QF = compose (IDEA_Q_F Key2,n,r),MESSAGES as Function of MESSAGES ,MESSAGES by A26, FUNCT_2:def 1, RELSET_1:11;
A28: m2 in MESSAGES by FINSEQ_1:def 11;
A29: QF . (PF . m1) = (QF * PF) . m1 by A9, FUNCT_2:21
.= (compose ((IDEA_P_F Key1,n,r) ^ (IDEA_Q_F Key2,n,r)),MESSAGES ) . m1 by A22, FUNCT_7:50
.= m1 by A1, A2, A3, A5, A10, A14, A13, A12, A11, Th48 ;
A30: m2 . 4 is_expressible_by n by A3, A10, A14, A13, A12, A11, Th47;
A31: ( m2 . 2 is_expressible_by n & m2 . 3 is_expressible_by n ) by A3, A10, A14, A13, A12, A11, Th47;
thus ((IDEA_QS ks2,n) * ((compose (IDEA_Q_F Key2,n,r),MESSAGES ) * ((IDEA_QE ke2,n) * ((IDEA_PE ke1,n) * ((compose (IDEA_P_F Key1,n,r),MESSAGES ) * (IDEA_PS ks1,n)))))) . m = (IDEA_QS ks2,n) . ((QF * ((IDEA_QE ke2,n) * ((IDEA_PE ke1,n) * (PF * (IDEA_PS ks1,n))))) . m) by A8, FUNCT_2:21
.= (IDEA_QS ks2,n) . (QF . (((IDEA_QE ke2,n) * ((IDEA_PE ke1,n) * (PF * (IDEA_PS ks1,n)))) . m)) by A8, FUNCT_2:21
.= (IDEA_QS ks2,n) . (QF . ((IDEA_QE ke2,n) . (((IDEA_PE ke1,n) * (PF * (IDEA_PS ks1,n))) . m))) by A8, FUNCT_2:21
.= (IDEA_QS ks2,n) . (QF . ((IDEA_QE ke2,n) . ((IDEA_PE ke1,n) . ((PF * (IDEA_PS ks1,n)) . m)))) by A8, FUNCT_2:21
.= (IDEA_QS ks2,n) . (QF . ((IDEA_QE ke2,n) . ((IDEA_PE ke1,n) . (PF . ((IDEA_PS ks1,n) . m))))) by A8, FUNCT_2:21
.= (IDEA_QS ks2,n) . (QF . (((IDEA_QE ke2,n) * (IDEA_PE ke1,n)) . m2)) by A28, FUNCT_2:21
.= (IDEA_QS ks2,n) . m1 by A2, A7, A23, A31, A30, A29, Th36
.= ((IDEA_QS ks2,n) * (IDEA_PS ks1,n)) . m by A8, FUNCT_2:21
.= m by A2, A3, A4, A6, Th35 ; :: thesis:

end;