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:
for m being FinSequence of NAT
for r being Element of NAT st lk >= r & (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 & ( 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 ) ) holds
(compose ((IDEA_P_F Key1,n,r) ^ (IDEA_Q_F Key2,n,r)),MESSAGES ) . m = m

proof

let m be FinSequence of NAT ; :: thesis:
defpred S₁[ Element of NAT ] means ( lk >= $1 & (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 & ( for i being Element of NAT st i <= $1 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 ) ) implies (compose ((IDEA_P_F Key1,n,$1) ^ (IDEA_Q_F Key2,n,$1)),MESSAGES ) . m = m );
A1: len (IDEA_P_F Key1,n,0 ) = 0 by Def17;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A3: S₁[k] ; :: thesis:
consider k1 being Element of NAT such that
A4: k1 = k + 1 ;
A5: dom (compose (IDEA_P_F Key1,n,k),MESSAGES ) = MESSAGES by Th44;
A6: rng (compose (IDEA_P_F Key1,n,k),MESSAGES ) c= MESSAGES by Th44;
A7: m in MESSAGES by FINSEQ_1:def 11;
then (compose (IDEA_P_F Key1,n,k),MESSAGES ) . m in rng (compose (IDEA_P_F Key1,n,k),MESSAGES ) by A5, FUNCT_1:def 5;
then reconsider M = (compose (IDEA_P_F Key1,n,k),MESSAGES ) . m as FinSequence of NAT by A6, FINSEQ_1:def 11;
assume that
A8: lk >= k + 1 and
A9: (2 to_power n) + 1 is prime and
A10: ( 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 ) and
A11: for i being Element of NAT st i <= k + 1 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 ) ; :: thesis:
A12: ( len M >= 4 & M . 1 is_expressible_by n ) by A10, Th47;
A13: width Key1 = 6 by A8, MATRIX_1:24;
then 1 in Seg (width Key1) by FINSEQ_1:3;
then A14: (Line Key1,(k + 1)) . 1 = Key1 * k1,1 by A4, MATRIX_1:def 8;
then A15: (Line Key1,(k + 1)) . 1 is_expressible_by n by A11, A4;
A16: width Key2 = 6 by A8, MATRIX_1:24;
then 5 in Seg (width Key2) by FINSEQ_1:3;
then A17: (Line Key2,(k + 1)) . 5 = Key2 * k1,5 by A4, MATRIX_1:def 8;
3 in Seg (width Key1) by A13, FINSEQ_1:3;
then A18: (Line Key1,(k + 1)) . 3 = Key1 * k1,3 by A4, MATRIX_1:def 8;
then A19: (Line Key1,(k + 1)) . 3 is_expressible_by n by A11, A4;
2 in Seg (width Key1) by A13, FINSEQ_1:3;
then A20: (Line Key1,(k + 1)) . 2 = Key1 * k1,2 by A4, MATRIX_1:def 8;
then A21: (Line Key1,(k + 1)) . 2 is_expressible_by n by A11, A4;
3 in Seg (width Key2) by A16, FINSEQ_1:3;
then (Line Key2,(k + 1)) . 3 = Key2 * k1,3 by A4, MATRIX_1:def 8;
then A22: (Line Key2,(k + 1)) . 3 = NEG_MOD ((Line Key1,(k + 1)) . 2),n by A11, A4, A20;
2 in Seg (width Key2) by A16, FINSEQ_1:3;
then (Line Key2,(k + 1)) . 2 = Key2 * k1,2 by A4, MATRIX_1:def 8;
then A23: (Line Key2,(k + 1)) . 2 = NEG_MOD ((Line Key1,(k + 1)) . 3),n by A11, A4, A18;
5 in Seg (width Key1) by A13, FINSEQ_1:3;
then (Line Key1,(k + 1)) . 5 = Key1 * k1,5 by A4, MATRIX_1:def 8;
then A24: (Line Key2,(k + 1)) . 5 = (Line Key1,(k + 1)) . 5 by A11, A4, A17;
A25: M . 4 is_expressible_by n by A10, Th47;
A26: ( M . 2 is_expressible_by n & M . 3 is_expressible_by n ) by A10, Th47;
4 in Seg (width Key1) by A13, FINSEQ_1:3;
then A27: (Line Key1,(k + 1)) . 4 = Key1 * k1,4 by A4, MATRIX_1:def 8;
then A28: (Line Key1,(k + 1)) . 4 is_expressible_by n by A11, A4;
4 in Seg (width Key2) by A16, FINSEQ_1:3;
then (Line Key2,(k + 1)) . 4 = Key2 * k1,4 by A4, MATRIX_1:def 8;
then A29: (Line Key2,(k + 1)) . 4 = INV_MOD ((Line Key1,(k + 1)) . 4),n by A11, A4, A27;
6 in Seg (width Key2) by A16, FINSEQ_1:3;
then A30: (Line Key2,(k + 1)) . 6 = Key2 * k1,6 by A4, MATRIX_1:def 8;
6 in Seg (width Key1) by A13, FINSEQ_1:3;
then (Line Key1,(k + 1)) . 6 = Key1 * k1,6 by A4, MATRIX_1:def 8;
then A31: (Line Key2,(k + 1)) . 6 = (Line Key1,(k + 1)) . 6 by A11, A4, A30;
dom ((IDEA_Q (Line Key2,(k + 1)),n) * (IDEA_P (Line Key1,(k + 1)),n)) = MESSAGES by FUNCT_2:def 1;
then A32: dom (((IDEA_Q (Line Key2,(k + 1)),n) * (IDEA_P (Line Key1,(k + 1)),n)) * (compose (IDEA_P_F Key1,n,k),MESSAGES )) = MESSAGES by A6, A5, RELAT_1:46;
rng (compose ((IDEA_P_F Key1,n,k) ^ (<*(IDEA_P (Line Key1,(k + 1)),n)*> ^ <*(IDEA_Q (Line Key2,(k + 1)),n)*>)),MESSAGES ) = rng (compose (((IDEA_P_F Key1,n,k) ^ <*(IDEA_P (Line Key1,(k + 1)),n)*>) ^ <*(IDEA_Q (Line Key2,(k + 1)),n)*>),MESSAGES ) by FINSEQ_1:45
.= rng ((IDEA_Q (Line Key2,(k + 1)),n) * (compose ((IDEA_P_F Key1,n,k) ^ <*(IDEA_P (Line Key1,(k + 1)),n)*>),MESSAGES )) by FUNCT_7:43 ;
then A33: rng (compose ((IDEA_P_F Key1,n,k) ^ (<*(IDEA_P (Line Key1,(k + 1)),n)*> ^ <*(IDEA_Q (Line Key2,(k + 1)),n)*>)),MESSAGES ) c= MESSAGES by RELAT_1:def 19;
1 in Seg (width Key2) by A16, FINSEQ_1:3;
then (Line Key2,(k + 1)) . 1 = Key2 * k1,1 by A4, MATRIX_1:def 8;
then A34: (Line Key2,(k + 1)) . 1 = INV_MOD ((Line Key1,(k + 1)) . 1),n by A11, A4, A14;
A35: k + 1 >= k by NAT_1:11;
A36: for i being Element of NAT st i <= k 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 )

proof

let i be Element of NAT ; :: thesis:
assume i <= k ; :: thesis:
then i <= k + 1 by A35, XXREAL_0:2;
hence ( 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 ) by A11; :: thesis:

end;

(compose ((IDEA_P_F Key1,n,(k + 1)) ^ (IDEA_Q_F Key2,n,(k + 1))),MESSAGES ) . m = (compose (((IDEA_P_F Key1,n,k) ^ <*(IDEA_P (Line Key1,(k + 1)),n)*>) ^ (IDEA_Q_F Key2,n,(k + 1))),MESSAGES ) . m by Th37
.= (compose (((IDEA_P_F Key1,n,k) ^ <*(IDEA_P (Line Key1,(k + 1)),n)*>) ^ (<*(IDEA_Q (Line Key2,(k + 1)),n)*> ^ (IDEA_Q_F Key2,n,k))),MESSAGES ) . m by Th38
.= (compose ((((IDEA_P_F Key1,n,k) ^ <*(IDEA_P (Line Key1,(k + 1)),n)*>) ^ <*(IDEA_Q (Line Key2,(k + 1)),n)*>) ^ (IDEA_Q_F Key2,n,k)),MESSAGES ) . m by FINSEQ_1:45
.= (compose (((IDEA_P_F Key1,n,k) ^ (<*(IDEA_P (Line Key1,(k + 1)),n)*> ^ <*(IDEA_Q (Line Key2,(k + 1)),n)*>)) ^ (IDEA_Q_F Key2,n,k)),MESSAGES ) . m by FINSEQ_1:45
.= ((compose (IDEA_Q_F Key2,n,k),MESSAGES ) * (compose ((IDEA_P_F Key1,n,k) ^ (<*(IDEA_P (Line Key1,(k + 1)),n)*> ^ <*(IDEA_Q (Line Key2,(k + 1)),n)*>)),MESSAGES )) . m by A33, FUNCT_7:50
.= ((compose (IDEA_Q_F Key2,n,k),MESSAGES ) * ((compose (<*(IDEA_P (Line Key1,(k + 1)),n)*> ^ <*(IDEA_Q (Line Key2,(k + 1)),n)*>),MESSAGES ) * (compose (IDEA_P_F Key1,n,k),MESSAGES ))) . m by A6, FUNCT_7:50
.= ((compose (IDEA_Q_F Key2,n,k),MESSAGES ) * ((compose <*(IDEA_P (Line Key1,(k + 1)),n),(IDEA_Q (Line Key2,(k + 1)),n)*>,MESSAGES ) * (compose (IDEA_P_F Key1,n,k),MESSAGES ))) . m by FINSEQ_1:def 9
.= ((compose (IDEA_Q_F Key2,n,k),MESSAGES ) * ((((IDEA_Q (Line Key2,(k + 1)),n) * (IDEA_P (Line Key1,(k + 1)),n)) * (id MESSAGES )) * (compose (IDEA_P_F Key1,n,k),MESSAGES ))) . m by FUNCT_7:53
.= ((compose (IDEA_Q_F Key2,n,k),MESSAGES ) * (((IDEA_Q (Line Key2,(k + 1)),n) * (IDEA_P (Line Key1,(k + 1)),n)) * (compose (IDEA_P_F Key1,n,k),MESSAGES ))) . m by FUNCT_2:23
.= (compose (IDEA_Q_F Key2,n,k),MESSAGES ) . ((((IDEA_Q (Line Key2,(k + 1)),n) * (IDEA_P (Line Key1,(k + 1)),n)) * (compose (IDEA_P_F Key1,n,k),MESSAGES )) . m) by A32, A7, FUNCT_1:23
.= (compose (IDEA_Q_F Key2,n,k),MESSAGES ) . (((IDEA_Q (Line Key2,(k + 1)),n) * (IDEA_P (Line Key1,(k + 1)),n)) . ((compose (IDEA_P_F Key1,n,k),MESSAGES ) . m)) by A5, A7, FUNCT_1:23
.= (compose (IDEA_Q_F Key2,n,k),MESSAGES ) . ((compose (IDEA_P_F Key1,n,k),MESSAGES ) . m) by A9, A12, A26, A25, A15, A21, A19, A28, A34, A23, A22, A29, A24, A31, Th34
.= ((compose (IDEA_Q_F Key2,n,k),MESSAGES ) * (compose (IDEA_P_F Key1,n,k),MESSAGES )) . m by A5, A7, FUNCT_1:23
.= m by A3, A8, A9, A10, A35, A36, A6, FUNCT_7:50, XXREAL_0:2 ;
hence (compose ((IDEA_P_F Key1,n,(k + 1)) ^ (IDEA_Q_F Key2,n,(k + 1))),MESSAGES ) . m = m ; :: thesis:

end;

len (IDEA_Q_F Key2,n,0 ) = 0 by Def18;
then IDEA_Q_F Key2,n,0 = {} ;
then (IDEA_P_F Key1,n,0 ) ^ (IDEA_Q_F Key2,n,0 ) = IDEA_P_F Key1,n,0 by FINSEQ_1:47
.= {} by A1 ;
then ( m in MESSAGES & compose ((IDEA_P_F Key1,n,0 ) ^ (IDEA_Q_F Key2,n,0 )),MESSAGES = id MESSAGES ) by FINSEQ_1:def 11, FUNCT_7:41;
then A37: S₁[ 0 ] by FUNCT_1:35;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A37, A2); :: thesis:

end;

hence for r being Element of NAT
for m being FinSequence of NAT st lk >= r & (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 & ( 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 ) ) holds
(compose ((IDEA_P_F Key1,n,r) ^ (IDEA_Q_F Key2,n,r)),MESSAGES ) . m = m ; :: thesis: