let n be non empty Element of NAT ; :: thesis:
let lk be Element of NAT ; :: thesis:
let Key be Matrix of lk,6, NAT ; :: thesis:
let r be Element of 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 & 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:
A3: m in MESSAGES by FINSEQ_1:def 11;

per cases ;

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:41
.= m by A3, FUNCT_1:35 ;
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; :: thesis:

end;

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

consider r1 being Integer such that
A5: r1 = r - 1 ;
1 <= r by A4, NAT_1:14;
then 1 - 1 <= r - 1 by XREAL_1:11;
then reconsider r1 = r1 as Element of NAT by A5, INT_1:16;
IDEA_P_F Key,n,(r1 + 1) = (IDEA_P_F Key,n,r1) ^ <*(IDEA_P (Line Key,(r1 + 1)),n)*> by Th37;
then A6: compose (IDEA_P_F Key,n,r),MESSAGES = (IDEA_P (Line Key,r),n) * (compose (IDEA_P_F Key,n,r1),MESSAGES ) by A5, FUNCT_7:43;
then m in dom ((IDEA_P (Line Key,r),n) * (compose (IDEA_P_F Key,n,r1),MESSAGES )) by A3, Th44;
then A7: M = (IDEA_P (Line Key,r),n) . ((compose (IDEA_P_F Key,n,r1),MESSAGES ) . m) by A1, A6, FUNCT_1:22;
A8: ( dom (compose (IDEA_P_F Key,n,r1),MESSAGES ) = MESSAGES & rng (compose (IDEA_P_F Key,n,r1),MESSAGES ) c= MESSAGES ) by Th44;
then (compose (IDEA_P_F Key,n,r1),MESSAGES ) . m in rng (compose (IDEA_P_F Key,n,r1),MESSAGES ) by A3, FUNCT_1:def 5;
then reconsider M1 = (compose (IDEA_P_F Key,n,r1),MESSAGES ) . m as FinSequence of NAT by A8, FINSEQ_1:def 11;
A9: m in MESSAGES by FINSEQ_1:def 11;
defpred S₁[ Element of NAT ] means for M being FinSequence of NAT st M = (compose (IDEA_P_F Key,n,$1),MESSAGES ) . m holds
len M >= 4;
A10: S₁[ 0 ]

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

end;

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

let k be Element of NAT ; :: thesis:
assume A13: S₁[k] ; :: thesis:
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 Th37;
then A14: M = ((IDEA_P (Line Key,(k + 1)),n) * (compose (IDEA_P_F Key,n,k),MESSAGES )) . m by FUNCT_7:43;
A15: ( dom (compose (IDEA_P_F Key,n,k),MESSAGES ) = MESSAGES & rng (compose (IDEA_P_F Key,n,k),MESSAGES ) c= MESSAGES ) by Th44;
then (compose (IDEA_P_F Key,n,k),MESSAGES ) . m in rng (compose (IDEA_P_F Key,n,k),MESSAGES ) by A9, FUNCT_1:def 5;
then reconsider M1 = (compose (IDEA_P_F Key,n,k),MESSAGES ) . m as FinSequence of NAT by A15, FINSEQ_1:def 11;
A16: len M1 >= 4 by A13;
dom ((IDEA_P (Line Key,(k + 1)),n) * (compose (IDEA_P_F Key,n,k),MESSAGES )) = MESSAGES

rng (compose (IDEA_P_F Key,n,k),MESSAGES ) c= dom (IDEA_P (Line Key,(k + 1)),n) by A15, FUNCT_2:def 1;
hence dom ((IDEA_P (Line Key,(k + 1)),n) * (compose (IDEA_P_F Key,n,k),MESSAGES )) = MESSAGES by A15, RELAT_1:46; :: thesis:

end;

then M = (IDEA_P (Line Key,(k + 1)),n) . ((compose (IDEA_P_F Key,n,k),MESSAGES ) . m) by A9, A14, FUNCT_1:22;
hence len M >= 4 by A16, Th43; :: thesis:

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A10, A12);
then len M1 >= 4 ;
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 A7, Th43; :: thesis:

end;