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 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 ; :: 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 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); :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( (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; :: 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 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 ; :: 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 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); :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( (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; :: thesis: verum