let A be 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 s being Element of Funcs (X,INT) holds (. x) . s = s . x
let X be 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 s being Element of Funcs (X,INT) holds (. x) . s = s . x
let T be Subset of (Funcs (X,INT)); for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T
for x being Variable of f
for s being Element of Funcs (X,INT) holds (. x) . s = s . x
let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; for x being Variable of f
for s being Element of Funcs (X,INT) holds (. x) . s = s . x
let x be Variable of f; for s being Element of Funcs (X,INT) holds (. x) . s = s . x
let s be Element of Funcs (X,INT); (. x) . s = s . x
thus (. x) . s =
s . ((x ^ (A,f)) . s)
by Def19
.=
s . x
; verum