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 DEFvarexp
.= s . x by FUNCOP_1:13 ; :: thesis: verum