:: deftheorem defines *= AOFA_I00:def 52 :
for A being Euclidean preIfWhileAlgebra
for X being non empty countable set
for T being Subset of (Funcs (X,INT))
for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T
for x being Variable of f
for i being Integer holds x *= i = x := ((. x) * i);