let n be Nat; :: thesis: for m, k being FinSequence of NAT st len m >= 4 holds
( (IDEAoperationA (m,k,n)) . 1 is_expressible_by n & (IDEAoperationA (m,k,n)) . 2 is_expressible_by n & (IDEAoperationA (m,k,n)) . 3 is_expressible_by n & (IDEAoperationA (m,k,n)) . 4 is_expressible_by n )
let m, k be FinSequence of NAT ; :: thesis: ( len m >= 4 implies ( (IDEAoperationA (m,k,n)) . 1 is_expressible_by n & (IDEAoperationA (m,k,n)) . 2 is_expressible_by n & (IDEAoperationA (m,k,n)) . 3 is_expressible_by n & (IDEAoperationA (m,k,n)) . 4 is_expressible_by n ) )
assume A1: len m >= 4 ; :: thesis: ( (IDEAoperationA (m,k,n)) . 1 is_expressible_by n & (IDEAoperationA (m,k,n)) . 2 is_expressible_by n & (IDEAoperationA (m,k,n)) . 3 is_expressible_by n & (IDEAoperationA (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:1;
then 1 in dom m by FINSEQ_1:def 3;
then A2: (IDEAoperationA (m,k,n)) . 1 = MUL_MOD ((m . 1),(k . 1),n) by Def11;
3 <= len m by A1, XXREAL_0:2;
then 3 in Seg (len m) by FINSEQ_1:1;
then 3 in dom m by FINSEQ_1:def 3;
then A3: (IDEAoperationA (m,k,n)) . 3 = ADD_MOD ((m . 3),(k . 3),n) by Def11;
2 <= len m by A1, XXREAL_0:2;
then 2 in Seg (len m) by FINSEQ_1:1;
then 2 in dom m by FINSEQ_1:def 3;
then A4: (IDEAoperationA (m,k,n)) . 2 = ADD_MOD ((m . 2),(k . 2),n) by Def11;
4 in Seg (len m) by A1, FINSEQ_1:1;
then 4 in dom m by FINSEQ_1:def 3;
then (IDEAoperationA (m,k,n)) . 4 = MUL_MOD ((m . 4),(k . 4),n) by Def11;
hence ( (IDEAoperationA (m,k,n)) . 1 is_expressible_by n & (IDEAoperationA (m,k,n)) . 2 is_expressible_by n & (IDEAoperationA (m,k,n)) . 3 is_expressible_by n & (IDEAoperationA (m,k,n)) . 4 is_expressible_by n ) by A2, A4, A3, Th15, Th24; :: thesis: verum