let A be Euclidean preIfWhileAlgebra; :: thesis: 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 ; :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: for s being Element of Funcs (X,INT) holds (. x) . s = s . x

let s be Element of Funcs (X,INT); :: thesis: (. x) . s = s . x

thus (. x) . s = s . ((x ^ (A,f)) . s) by Def19

.= s . x ; :: thesis: verum

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 ; :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: for s being Element of Funcs (X,INT) holds (. x) . s = s . x

let s be Element of Funcs (X,INT); :: thesis: (. x) . s = s . x

thus (. x) . s = s . ((x ^ (A,f)) . s) by Def19

.= s . x ; :: thesis: verum