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, y being Variable of f holds

( (f . (s,(x *= y))) . x = (s . x) * (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 ; :: 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, y being Variable of f holds

( (f . (s,(x *= y))) . x = (s . x) * (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); :: thesis: 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) * (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)); :: thesis: 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) * (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; :: thesis: for x, y being Variable of f holds

( (f . (s,(x *= y))) . x = (s . x) * (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; :: thesis: ( (f . (s,(x *= y))) . x = (s . x) * (s . y) & ( for z being Element of X st z <> x holds

(f . (s,(x *= y))) . z = s . z ) )

A1: dom ((. x) (#) (. y)) = Funcs (X,INT) by FUNCT_2:def 1;

(^ x) . s = x ;

hence (f . (s,(x *= y))) . x = ((. x) (#) (. y)) . s by Th24

.= ((. x) . s) * ((. y) . s) by A1, VALUED_1:def 4

.= (s . x) * ((. y) . s) by Th22

.= (s . x) * (s . y) by Th22 ;

:: thesis: for z being Element of X st z <> x holds

(f . (s,(x *= y))) . z = s . z

thus for z being Element of X st z <> x holds

(f . (s,(x *= y))) . z = s . z by Th26; :: 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, y being Variable of f holds

( (f . (s,(x *= y))) . x = (s . x) * (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 ; :: 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, y being Variable of f holds

( (f . (s,(x *= y))) . x = (s . x) * (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); :: thesis: 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) * (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)); :: thesis: 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) * (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; :: thesis: for x, y being Variable of f holds

( (f . (s,(x *= y))) . x = (s . x) * (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; :: thesis: ( (f . (s,(x *= y))) . x = (s . x) * (s . y) & ( for z being Element of X st z <> x holds

(f . (s,(x *= y))) . z = s . z ) )

A1: dom ((. x) (#) (. y)) = Funcs (X,INT) by FUNCT_2:def 1;

(^ x) . s = x ;

hence (f . (s,(x *= y))) . x = ((. x) (#) (. y)) . s by Th24

.= ((. x) . s) * ((. y) . s) by A1, VALUED_1:def 4

.= (s . x) * ((. y) . s) by Th22

.= (s . x) * (s . y) by Th22 ;

:: thesis: for z being Element of X st z <> x holds

(f . (s,(x *= y))) . z = s . z

thus for z being Element of X st z <> x holds

(f . (s,(x *= y))) . z = s . z by Th26; :: thesis: verum