let A be 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, y being Variable of f holds
( (f . (s,(x /= y))) . x = (s . x) div (s . y) & ( for z being Element of X st z <> x holds
(f . (s,(x /= y))) . z = s . z ) )
let X be 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, y being Variable of f holds
( (f . (s,(x /= y))) . x = (s . x) div (s . y) & ( for z being Element of X st z <> x holds
(f . (s,(x /= y))) . z = s . z ) )
let s be 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, y being Variable of f holds
( (f . (s,(x /= y))) . x = (s . x) div (s . y) & ( for z being Element of X st z <> x holds
(f . (s,(x /= y))) . z = s . z ) )
let T be Subset of (Funcs (X,INT)); for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T
for x, y being Variable of f holds
( (f . (s,(x /= y))) . x = (s . x) div (s . y) & ( for z being Element of X st z <> x holds
(f . (s,(x /= y))) . z = s . z ) )
let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; for x, y being Variable of f holds
( (f . (s,(x /= y))) . x = (s . x) div (s . y) & ( for z being Element of X st z <> x holds
(f . (s,(x /= y))) . z = s . z ) )
let x, y be Variable of f; ( (f . (s,(x /= y))) . x = (s . x) div (s . y) & ( for z being Element of X st z <> x holds
(f . (s,(x /= y))) . z = s . z ) )
A1:
x /= y = x /= (. y)
;
(. y) . s = s . y
by Th22;
hence
( (f . (s,(x /= y))) . x = (s . x) div (s . y) & ( for z being Element of X st z <> x holds
(f . (s,(x /= y))) . z = s . z ) )
by A1, Th46; verum