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: S₁[ 0 ]

proof

A2: len (IDEA_P_F Key1,n,0 ) = 0 by Def17;
A3: m in MESSAGES by FINSEQ_1:def 11;
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 A2 ;
then compose ((IDEA_P_F Key1,n,0 ) ^ (IDEA_Q_F Key2,n,0 )),MESSAGES = id MESSAGES by FUNCT_7:41;
hence S₁[ 0 ] by A3, FUNCT_1:35; :: thesis:

end;

A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A5: S₁[k] ; :: thesis:
assume that
A6: lk >= k + 1 and
A7: (2 to_power n) + 1 is prime and
A8: len m >= 4 and
A9: ( 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
A10: 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:
A11: k + 1 >= k by NAT_1:11;
A12: 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 A11, 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 A10; :: thesis:

end;

A13: rng (compose (IDEA_P_F Key1,n,k),MESSAGES ) c= MESSAGES by Th44;
A14: 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

proof

A15: 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 ;
A16: rng ((IDEA_Q (Line Key2,(k + 1)),n) * (compose ((IDEA_P_F Key1,n,k) ^ <*(IDEA_P (Line Key1,(k + 1)),n)*>),MESSAGES )) c= rng (IDEA_Q (Line Key2,(k + 1)),n)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in rng ((IDEA_Q (Line Key2,(k + 1)),n) * (compose ((IDEA_P_F Key1,n,k) ^ <*(IDEA_P (Line Key1,(k + 1)),n)*>),MESSAGES )) ; :: thesis:
hence a in rng (IDEA_Q (Line Key2,(k + 1)),n) by FUNCT_1:25; :: thesis:

end;

rng (IDEA_Q (Line Key2,(k + 1)),n) c= MESSAGES by RELAT_1:def 19;
hence 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 A15, A16, XBOOLE_1:1; :: thesis:

end;

A17: dom (compose (IDEA_P_F Key1,n,k),MESSAGES ) = MESSAGES by Th44;
A18: dom (((IDEA_Q (Line Key2,(k + 1)),n) * (IDEA_P (Line Key1,(k + 1)),n)) * (compose (IDEA_P_F Key1,n,k),MESSAGES )) = MESSAGES

proof

dom ((IDEA_Q (Line Key2,(k + 1)),n) * (IDEA_P (Line Key1,(k + 1)),n)) = MESSAGES by FUNCT_2:def 1;
hence 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 A13, A17, RELAT_1:46; :: thesis:

end;

A19: 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 A17, FUNCT_1:def 5;
then reconsider M = (compose (IDEA_P_F Key1,n,k),MESSAGES ) . m as FinSequence of NAT by A13, FINSEQ_1:def 11;
A20: ( 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 ) by A8, A9, Th47;
( width Key1 = 6 & width Key2 = 6 ) by A6, MATRIX_1:24;
then A21: ( 1 in Seg (width Key1) & 2 in Seg (width Key1) & 3 in Seg (width Key1) & 4 in Seg (width Key1) & 5 in Seg (width Key1) & 6 in Seg (width Key1) & 1 in Seg (width Key2) & 2 in Seg (width Key2) & 3 in Seg (width Key2) & 4 in Seg (width Key2) & 5 in Seg (width Key2) & 6 in Seg (width Key2) ) by FINSEQ_1:3;
consider k1 being Element of NAT such that
A22: k1 = k + 1 ;
( (Line Key1,(k + 1)) . 1 = Key1 * k1,1 & (Line Key1,(k + 1)) . 2 = Key1 * k1,2 & (Line Key1,(k + 1)) . 3 = Key1 * k1,3 & (Line Key1,(k + 1)) . 4 = Key1 * k1,4 & (Line Key1,(k + 1)) . 5 = Key1 * k1,5 & (Line Key1,(k + 1)) . 6 = Key1 * k1,6 & (Line Key2,(k + 1)) . 1 = Key2 * k1,1 & (Line Key2,(k + 1)) . 2 = Key2 * k1,2 & (Line Key2,(k + 1)) . 3 = Key2 * k1,3 & (Line Key2,(k + 1)) . 4 = Key2 * k1,4 & (Line Key2,(k + 1)) . 5 = Key2 * k1,5 & (Line Key2,(k + 1)) . 6 = Key2 * k1,6 ) by A21, A22, MATRIX_1:def 8;
then A23: ( (Line Key1,(k + 1)) . 1 is_expressible_by n & (Line Key1,(k + 1)) . 2 is_expressible_by n & (Line Key1,(k + 1)) . 3 is_expressible_by n & (Line Key1,(k + 1)) . 4 is_expressible_by n & (Line Key1,(k + 1)) . 5 is_expressible_by n & (Line Key1,(k + 1)) . 6 is_expressible_by n & (Line Key2,(k + 1)) . 1 = INV_MOD ((Line Key1,(k + 1)) . 1),n & (Line Key2,(k + 1)) . 2 = NEG_MOD ((Line Key1,(k + 1)) . 3),n & (Line Key2,(k + 1)) . 3 = NEG_MOD ((Line Key1,(k + 1)) . 2),n & (Line Key2,(k + 1)) . 4 = INV_MOD ((Line Key1,(k + 1)) . 4),n & (Line Key2,(k + 1)) . 5 = (Line Key1,(k + 1)) . 5 & (Line Key2,(k + 1)) . 6 = (Line Key1,(k + 1)) . 6 ) by A10, A22;
(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 A14, 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 A13, 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 A18, A19, 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 A17, A19, FUNCT_1:23
.= (compose (IDEA_Q_F Key2,n,k),MESSAGES ) . ((compose (IDEA_P_F Key1,n,k),MESSAGES ) . m) by A7, A20, A23, Th34
.= ((compose (IDEA_Q_F Key2,n,k),MESSAGES ) * (compose (IDEA_P_F Key1,n,k),MESSAGES )) . m by A17, A19, FUNCT_1:23
.= m by A5, A6, A7, A8, A9, A11, A12, A13, 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;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A4); :: 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: