let n be Element of 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:3;
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:3;
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:3;
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:3;
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, Th16, Th25; :: thesis: verum