let A be Euclidean preIfWhileAlgebra; 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 v being INT-Variable of A,f
for t being INT-Expression of A,f holds
( (f . (s,(v := t))) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . (s,(v := t))) . z = s . z ) )
let X be 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 v being INT-Variable of A,f
for t being INT-Expression of A,f holds
( (f . (s,(v := t))) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . (s,(v := t))) . z = s . z ) )
let s be 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 v being INT-Variable of A,f
for t being INT-Expression of A,f holds
( (f . (s,(v := t))) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . (s,(v := t))) . z = s . z ) )
let T be Subset of (Funcs (X,INT)); for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T
for v being INT-Variable of A,f
for t being INT-Expression of A,f holds
( (f . (s,(v := t))) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . (s,(v := t))) . z = s . z ) )
let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; for v being INT-Variable of A,f
for t being INT-Expression of A,f holds
( (f . (s,(v := t))) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . (s,(v := t))) . z = s . z ) )
let v be INT-Variable of A,f; for t being INT-Expression of A,f holds
( (f . (s,(v := t))) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . (s,(v := t))) . z = s . z ) )
let t be INT-Expression of A,f; ( (f . (s,(v := t))) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . (s,(v := t))) . z = s . z ) )
set Y = { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) } ;
v,t form_assignment_wrt f
by Def22;
then consider I0 being Element of A such that
A1:
I0 in ElementaryInstructions A
and
A2:
for s being Element of Funcs (X,INT) holds f . (s,I0) = s +* ((v . s),(t . s))
;
I0 in { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) }
by A1, A2;
then
v := t in { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) }
;
then
ex I being Element of A st
( v := t = I & I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) )
;
then A3:
f . (s,(v := t)) = s +* ((v . s),(t . s))
;
dom s = X
by FUNCT_2:def 1;
hence
( (f . (s,(v := t))) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . (s,(v := t))) . z = s . z ) )
by A3, FUNCT_7:31, FUNCT_7:32; verum