theorem Th43: :: AOFA_I00:43

for A being Euclidean preIfWhileAlgebra
for X being non empty countable set
for s being Element of Funcs (X,INT)
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 t being INT-Expression of A,f holds
( (f . (s,(x %= t))) . x = (s . x) mod (t . s) & ( for z being Element of X st z <> x holds
(f . (s,(x %= t))) . z = s . z ) )