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