let m, k be FinSequence of NAT ; :: thesis: for n being non empty Element of NAT st len m >= 4 holds
( (IDEAoperationB m,k,n) . 1 is_expressible_by n & (IDEAoperationB m,k,n) . 2 is_expressible_by n & (IDEAoperationB m,k,n) . 3 is_expressible_by n & (IDEAoperationB m,k,n) . 4 is_expressible_by n )
let n be non empty Element of NAT ; :: thesis: ( len m >= 4 implies ( (IDEAoperationB m,k,n) . 1 is_expressible_by n & (IDEAoperationB m,k,n) . 2 is_expressible_by n & (IDEAoperationB m,k,n) . 3 is_expressible_by n & (IDEAoperationB m,k,n) . 4 is_expressible_by n ) )
assume A1: len m >= 4 ; :: thesis: ( (IDEAoperationB m,k,n) . 1 is_expressible_by n & (IDEAoperationB m,k,n) . 2 is_expressible_by n & (IDEAoperationB m,k,n) . 3 is_expressible_by n & (IDEAoperationB m,k,n) . 4 is_expressible_by n )
then 1 <= len m by XXREAL_0:2;
then 1 in Seg (len m) by FINSEQ_1:3;
then 1 in dom m by FINSEQ_1:def 3;
then (IDEAoperationB m,k,n) . 1 = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n))) by Def12;
then A2: (IDEAoperationB m,k,n) . 1 < 2 to_power n by BINARI_3:1;
3 <= len m by A1, XXREAL_0:2;
then 3 in Seg (len m) by FINSEQ_1:3;
then 3 in dom m by FINSEQ_1:def 3;
then (IDEAoperationB m,k,n) . 3 = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n))) by Def12;
then A3: (IDEAoperationB m,k,n) . 3 < 2 to_power n by BINARI_3:1;
2 <= len m by A1, XXREAL_0:2;
then 2 in Seg (len m) by FINSEQ_1:3;
then 2 in dom m by FINSEQ_1:def 3;
then (IDEAoperationB m,k,n) . 2 = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n))) by Def12;
then A4: (IDEAoperationB m,k,n) . 2 < 2 to_power n by BINARI_3:1;
4 in Seg (len m) by A1, FINSEQ_1:3;
then 4 in dom m by FINSEQ_1:def 3;
then (IDEAoperationB m,k,n) . 4 = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n))) by Def12;
then (IDEAoperationB m,k,n) . 4 < 2 to_power n by BINARI_3:1;
hence ( (IDEAoperationB m,k,n) . 1 is_expressible_by n & (IDEAoperationB m,k,n) . 2 is_expressible_by n & (IDEAoperationB m,k,n) . 3 is_expressible_by n & (IDEAoperationB m,k,n) . 4 is_expressible_by n ) by A2, A4, A3, Def3; :: thesis: verum