:: deftheorem Def11 defines IDEAoperationA IDEA_1:def 11 :
for n being Nat
for m, k, b₄ being FinSequence of NAT holds
( b₄ = IDEAoperationA (m,k,n) iff ( len b₄ = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies b₄ . i = MUL_MOD ((m . 1),(k . 1),n) ) & ( i = 2 implies b₄ . i = ADD_MOD ((m . 2),(k . 2),n) ) & ( i = 3 implies b₄ . i = ADD_MOD ((m . 3),(k . 3),n) ) & ( i = 4 implies b₄ . i = MUL_MOD ((m . 4),(k . 4),n) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b₄ . i = m . i ) ) ) ) );