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 & 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: 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
A5: ( 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
A6: ( ke1 . 1 is_expressible_by n & ke1 . 2 is_expressible_by n & ke1 . 3 is_expressible_by n & ke1 . 4 is_expressible_by n & ke1 . 5 is_expressible_by n & ke1 . 6 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:
A7: 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;
A8: len m1 = len (IDEAoperationA m,ks1,n) by Def19
.= len m by Def11 ;
( m1 . 1 = (IDEAoperationA m,ks1,n) . 1 & m1 . 2 = (IDEAoperationA m,ks1,n) . 2 & m1 . 3 = (IDEAoperationA m,ks1,n) . 3 & m1 . 4 = (IDEAoperationA m,ks1,n) . 4 ) by Def19;
then A9: ( m1 . 1 is_expressible_by n & m1 . 2 is_expressible_by n & m1 . 3 is_expressible_by n & m1 . 4 is_expressible_by n ) by A2, Th27;
A10: m1 in MESSAGES by FINSEQ_1:def 11;

per cases ;

suppose A11: r = 0 ; :: thesis:

then len (IDEA_P_F Key1,n,r) = 0 by Def17;
then A12: IDEA_P_F Key1,n,r = {} ;
len (IDEA_Q_F Key2,n,r) = 0 by A11, Def18;
then IDEA_Q_F Key2,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 A12
.= ((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 A7, FUNCT_2:21
.= (IDEA_QS ks2,n) . ((IDEA_QE ke2,n) . (((IDEA_PE ke1,n) * (IDEA_PS ks1,n)) . m)) by A7, FUNCT_2:21
.= (IDEA_QS ks2,n) . ((IDEA_QE ke2,n) . ((IDEA_PE ke1,n) . m1)) by A7, FUNCT_2:21
.= (IDEA_QS ks2,n) . (((IDEA_QE ke2,n) * (IDEA_PE ke1,n)) . m1) by A10, FUNCT_2:21
.= (IDEA_QS ks2,n) . ((IDEA_PS ks1,n) . m) by A2, A6, A8, A9, Th36
.= ((IDEA_QS ks2,n) * (IDEA_PS ks1,n)) . m by A7, FUNCT_2:21
.= m by A2, A3, A5, Th35 ;
:: thesis:

end;

suppose r <> 0 ; :: thesis:

then A13: ( IDEA_P_F Key1,n,r is FuncSequence of MESSAGES , MESSAGES & IDEA_Q_F Key2,n,r is FuncSequence of MESSAGES , MESSAGES ) by Th41, Th42;
compose (IDEA_P_F Key1,n,r),MESSAGES is Function of MESSAGES ,MESSAGES

proof

A14: ( firstdom (IDEA_P_F Key1,n,r) = MESSAGES & lastrng (IDEA_P_F Key1,n,r) c= MESSAGES ) by A13, FUNCT_7:def 9;
then ( IDEA_P_F Key1,n,r = {} implies rng (compose (IDEA_P_F Key1,n,r),MESSAGES ) = {} ) by FUNCT_7:def 6;
then rng (compose (IDEA_P_F Key1,n,r),MESSAGES ) c= lastrng (IDEA_P_F Key1,n,r) by FUNCT_7:61, XBOOLE_1:2;
then A15: rng (compose (IDEA_P_F Key1,n,r),MESSAGES ) c= MESSAGES by A14, XBOOLE_1:1;
dom (compose (IDEA_P_F Key1,n,r),MESSAGES ) = MESSAGES by A13, A14, FUNCT_7:64;
hence compose (IDEA_P_F Key1,n,r),MESSAGES is Function of MESSAGES ,MESSAGES by A15, FUNCT_2:def 1, RELSET_1:11; :: thesis:

end;

then reconsider PF = compose (IDEA_P_F Key1,n,r),MESSAGES as Function of MESSAGES ,MESSAGES ;
compose (IDEA_Q_F Key2,n,r),MESSAGES is Function of MESSAGES ,MESSAGES

proof

A16: ( firstdom (IDEA_Q_F Key2,n,r) = MESSAGES & lastrng (IDEA_Q_F Key2,n,r) c= MESSAGES ) by A13, FUNCT_7:def 9;
then ( IDEA_Q_F Key2,n,r = {} implies rng (compose (IDEA_Q_F Key2,n,r),MESSAGES ) = {} ) by FUNCT_7:def 6;
then rng (compose (IDEA_Q_F Key2,n,r),MESSAGES ) c= lastrng (IDEA_Q_F Key2,n,r) by FUNCT_7:61, XBOOLE_1:2;
then A17: rng (compose (IDEA_Q_F Key2,n,r),MESSAGES ) c= MESSAGES by A16, XBOOLE_1:1;
dom (compose (IDEA_Q_F Key2,n,r),MESSAGES ) = MESSAGES by A13, A16, FUNCT_7:64;
hence compose (IDEA_Q_F Key2,n,r),MESSAGES is Function of MESSAGES ,MESSAGES by A17, FUNCT_2:def 1, RELSET_1:11; :: thesis:

end;

then reconsider QF = compose (IDEA_Q_F Key2,n,r),MESSAGES as Function of MESSAGES ,MESSAGES ;
A18: ( rng PF c= MESSAGES & rng QF c= MESSAGES ) by RELAT_1:def 19;
PF . m1 in MESSAGES by A10, FUNCT_2:7;
then reconsider m2 = PF . m1 as FinSequence of NAT by FINSEQ_1:def 11;
A19: ( len m2 >= 4 & m2 . 1 is_expressible_by n & m2 . 2 is_expressible_by n & m2 . 3 is_expressible_by n & m2 . 4 is_expressible_by n ) by A2, A8, A9, Th47;
A20: m2 in MESSAGES by FINSEQ_1:def 11;
A21: QF . (PF . m1) = m1

proof

thus QF . (PF . m1) = (QF * PF) . m1 by A10, FUNCT_2:21
.= (compose ((IDEA_P_F Key1,n,r) ^ (IDEA_Q_F Key2,n,r)),MESSAGES ) . m1 by A18, FUNCT_7:50
.= m1 by A1, A2, A4, A8, A9, Th48 ; :: thesis:

end;

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 A7, FUNCT_2:21
.= (IDEA_QS ks2,n) . (QF . (((IDEA_QE ke2,n) * ((IDEA_PE ke1,n) * (PF * (IDEA_PS ks1,n)))) . m)) by A7, FUNCT_2:21
.= (IDEA_QS ks2,n) . (QF . ((IDEA_QE ke2,n) . (((IDEA_PE ke1,n) * (PF * (IDEA_PS ks1,n))) . m))) by A7, FUNCT_2:21
.= (IDEA_QS ks2,n) . (QF . ((IDEA_QE ke2,n) . ((IDEA_PE ke1,n) . ((PF * (IDEA_PS ks1,n)) . m)))) by A7, FUNCT_2:21
.= (IDEA_QS ks2,n) . (QF . ((IDEA_QE ke2,n) . ((IDEA_PE ke1,n) . (PF . ((IDEA_PS ks1,n) . m))))) by A7, FUNCT_2:21
.= (IDEA_QS ks2,n) . (QF . (((IDEA_QE ke2,n) * (IDEA_PE ke1,n)) . m2)) by A20, FUNCT_2:21
.= (IDEA_QS ks2,n) . m1 by A2, A6, A19, A21, Th36
.= ((IDEA_QS ks2,n) * (IDEA_PS ks1,n)) . m by A7, FUNCT_2:21
.= m by A2, A3, A5, Th35 ; :: thesis:

end;