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

end;

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

consider r1 being Integer such that
A6: r1 = r - 1 ;
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;
A7: m in MESSAGES by FINSEQ_1:def 11;
A8: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis:
A9: dom (compose (IDEA_P_F Key,n,k),MESSAGES ) = MESSAGES by Th44;
A10: rng (compose (IDEA_P_F Key,n,k),MESSAGES ) c= MESSAGES by Th44;
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:46;
(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 5;
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 Th37;
then M = ((IDEA_P (Line Key,(k + 1)),n) * (compose (IDEA_P_F Key,n,k),MESSAGES )) . m by FUNCT_7:43;
then M = (IDEA_P (Line Key,(k + 1)),n) . ((compose (IDEA_P_F Key,n,k),MESSAGES ) . m) by A7, A11, FUNCT_1:22;
hence len M >= 4 by A12, Th43; :: thesis:

end;

1 <= r by A5, NAT_1:14;
then 1 - 1 <= r - 1 by XREAL_1:11;
then reconsider r1 = r1 as Element of NAT by A6, INT_1:16;
dom (compose (IDEA_P_F Key,n,r1),MESSAGES ) = MESSAGES by Th44;
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 5;
rng (compose (IDEA_P_F Key,n,r1),MESSAGES ) c= MESSAGES by Th44;
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:41
.= m by A7, FUNCT_1:35 ;
hence len M >= 4 by A2; :: thesis:

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(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 Th37;
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:43;
then m in dom ((IDEA_P (Line Key,r),n) * (compose (IDEA_P_F Key,n,r1),MESSAGES )) by A4, Th44;
then M = (IDEA_P (Line Key,r),n) . ((compose (IDEA_P_F Key,n,r1),MESSAGES ) . m) by A1, A17, FUNCT_1:22;
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, Th43; :: thesis:

end;

end;