let A be Euclidean preIfWhileAlgebra; :: thesis: 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) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

let X be non empty countable set ; :: thesis: 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) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

let s be Element of Funcs (X,INT); :: 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 t being INT-Expression of A,f holds

( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

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 t being INT-Expression of A,f holds

( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; :: thesis: for x being Variable of f

for t being INT-Expression of A,f holds

( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

let x be Variable of f; :: thesis: for t being INT-Expression of A,f holds

( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

let t be INT-Expression of A,f; :: thesis: ( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

A1: (^ x) . s = x ;

A2: (. x) . s = s . x by Th22;

((. x) div t) . s = ((. x) . s) div (t . s) by Def29;

hence ( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) ) by A1, A2, Th24; :: thesis: verum

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) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

let X be non empty countable set ; :: thesis: 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) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

let s be Element of Funcs (X,INT); :: 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 t being INT-Expression of A,f holds

( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

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 t being INT-Expression of A,f holds

( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; :: thesis: for x being Variable of f

for t being INT-Expression of A,f holds

( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

let x be Variable of f; :: thesis: for t being INT-Expression of A,f holds

( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

let t be INT-Expression of A,f; :: thesis: ( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) )

A1: (^ x) . s = x ;

A2: (. x) . s = s . x by Th22;

((. x) div t) . s = ((. x) . s) div (t . s) by Def29;

hence ( (f . (s,(x /= t))) . x = (s . x) div (t . s) & ( for z being Element of X st z <> x holds

(f . (s,(x /= t))) . z = s . z ) ) by A1, A2, Th24; :: thesis: verum