:: deftheorem Def13 defines IDEAoperationC IDEA_1:def 13 :
for m, b₂ being FinSequence of NAT holds
( b₂ = IDEAoperationC m iff ( len b₂ = len m & ( for i being Nat st i in dom m holds
b₂ . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) ) );