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 by FUNCOP_1:13;
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