let n be non zero Nat; :: thesis: for M, m, k being FinSequence of NAT st M = (IDEA_P (k,n)) . m & len m >= 4 holds
( 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 )
let M, m, k be FinSequence of NAT ; :: thesis: ( M = (IDEA_P (k,n)) . m & len m >= 4 implies ( 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 ) )
assume that
A1: M = (IDEA_P (k,n)) . m and
A2: len m >= 4 ; :: thesis: ( 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 )
A3: len m = len (IDEAoperationB (m,k,n)) by Def12
.= len (IDEAoperationC (IDEAoperationB (m,k,n))) by Def13 ;
M = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n) by A1, Def15;
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, Def11, Th26; :: thesis: verum