let n be non zero Nat; :: thesis:
let lk be Nat; :: thesis:
let Key be Matrix of lk,6,NAT; :: thesis:
let r be Nat; :: thesis:
let M, m be FinSequence of NAT ; :: thesis:
assume that
A1: M = (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) . m and
A2: 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 ) ; :: thesis:
A4: m in MESSAGES by FINSEQ_1:def 11;

suppose r = 0 ; :: thesis:

then len (IDEA_P_F (Key,n,r)) = 0 by Def17;
then IDEA_P_F (Key,n,r) = {} ;
then M = (id MESSAGES) . m by A1, FUNCT_7:39
.= m by A4, FUNCT_1:18 ;
hence ( 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 A2, A3; :: thesis:

end;

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

consider r1 being Integer such that
A6: r1 = r - 1 ;
defpred S₁[ Nat] means for M being FinSequence of NAT st M = (compose ((IDEA_P_F (Key,n,$1)),MESSAGES)) . m holds
len M >= 4;
A7: m in MESSAGES by FINSEQ_1:def 11;
A8: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
A9: dom (compose ((IDEA_P_F (Key,n,k)),MESSAGES)) = MESSAGES by Th43;
A10: rng (compose ((IDEA_P_F (Key,n,k)),MESSAGES)) c= MESSAGES by Th43;
then rng (compose ((IDEA_P_F (Key,n,k)),MESSAGES)) c= dom (IDEA_P ((Line (Key,(k + 1))),n)) by FUNCT_2:def 1;
then A11: dom ((IDEA_P ((Line (Key,(k + 1))),n)) * (compose ((IDEA_P_F (Key,n,k)),MESSAGES))) = MESSAGES by A9, RELAT_1:27;
(compose ((IDEA_P_F (Key,n,k)),MESSAGES)) . m in rng (compose ((IDEA_P_F (Key,n,k)),MESSAGES)) by A7, A9, FUNCT_1:def 3;
then reconsider M1 = (compose ((IDEA_P_F (Key,n,k)),MESSAGES)) . m as FinSequence of NAT by A10, FINSEQ_1:def 11;
assume S₁[k] ; :: thesis:
then A12: len M1 >= 4 ;
let M be FinSequence of NAT ; :: thesis:
assume M = (compose ((IDEA_P_F (Key,n,(k + 1))),MESSAGES)) . m ; :: thesis:
then M = (compose (((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>),MESSAGES)) . m by Th36;
then M = ((IDEA_P ((Line (Key,(k + 1))),n)) * (compose ((IDEA_P_F (Key,n,k)),MESSAGES))) . m by FUNCT_7:41;
then M = (IDEA_P ((Line (Key,(k + 1))),n)) . ((compose ((IDEA_P_F (Key,n,k)),MESSAGES)) . m) by A7, A11, FUNCT_1:12;
hence len M >= 4 by A12, Th42; :: thesis:

end;

1 <= r by A5, NAT_1:14;
then 1 - 1 <= r - 1 by XREAL_1:9;
then reconsider r1 = r1 as Element of NAT by A6, INT_1:3;
dom (compose ((IDEA_P_F (Key,n,r1)),MESSAGES)) = MESSAGES by Th43;
then A13: (compose ((IDEA_P_F (Key,n,r1)),MESSAGES)) . m in rng (compose ((IDEA_P_F (Key,n,r1)),MESSAGES)) by A4, FUNCT_1:def 3;
rng (compose ((IDEA_P_F (Key,n,r1)),MESSAGES)) c= MESSAGES by Th43;
then reconsider M1 = (compose ((IDEA_P_F (Key,n,r1)),MESSAGES)) . m as FinSequence of NAT by A13, FINSEQ_1:def 11;
A14: S₁[ 0 ]

let M be FinSequence of NAT ; :: thesis:
len (IDEA_P_F (Key,n,0)) = 0 by Def17;
then A15: IDEA_P_F (Key,n,0) = {} ;
assume M = (compose ((IDEA_P_F (Key,n,0)),MESSAGES)) . m ; :: thesis:
then M = (id MESSAGES) . m by A15, FUNCT_7:39
.= m by A7, FUNCT_1:18 ;
hence len M >= 4 by A2; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A14, A8);
then A16: len M1 >= 4 ;
IDEA_P_F (Key,n,(r1 + 1)) = (IDEA_P_F (Key,n,r1)) ^ <*(IDEA_P ((Line (Key,(r1 + 1))),n))*> by Th36;
then A17: compose ((IDEA_P_F (Key,n,r)),MESSAGES) = (IDEA_P ((Line (Key,r)),n)) * (compose ((IDEA_P_F (Key,n,r1)),MESSAGES)) by A6, FUNCT_7:41;
then m in dom ((IDEA_P ((Line (Key,r)),n)) * (compose ((IDEA_P_F (Key,n,r1)),MESSAGES))) by A4, Th43;
then M = (IDEA_P ((Line (Key,r)),n)) . ((compose ((IDEA_P_F (Key,n,r1)),MESSAGES)) . m) by A1, A17, FUNCT_1:12;
hence ( 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 A16, Th42; :: thesis:

end;

end;