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 i being integer number
for x being Variable of f holds
( (f . (s,(x /= i))) . x = (s . x) div i & ( for z being Element of X st z <> x holds
(f . (s,(x /= i))) . 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 i being integer number
for x being Variable of f holds
( (f . (s,(x /= i))) . x = (s . x) div i & ( for z being Element of X st z <> x holds
(f . (s,(x /= i))) . 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 i being integer number
for x being Variable of f holds
( (f . (s,(x /= i))) . x = (s . x) div i & ( for z being Element of X st z <> x holds
(f . (s,(x /= i))) . z = s . z ) )
let T be Subset of (Funcs (X,INT)); :: thesis: for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T
for i being integer number
for x being Variable of f holds
( (f . (s,(x /= i))) . x = (s . x) div i & ( for z being Element of X st z <> x holds
(f . (s,(x /= i))) . z = s . z ) )
let f be Euclidean ExecutionFunction of A, Funcs (X,INT),T; :: thesis: for i being integer number
for x being Variable of f holds
( (f . (s,(x /= i))) . x = (s . x) div i & ( for z being Element of X st z <> x holds
(f . (s,(x /= i))) . z = s . z ) )
let i be integer number ; :: thesis: for x being Variable of f holds
( (f . (s,(x /= i))) . x = (s . x) div i & ( for z being Element of X st z <> x holds
(f . (s,(x /= i))) . z = s . z ) )
let x be Variable of f; :: thesis: ( (f . (s,(x /= i))) . x = (s . x) div i & ( for z being Element of X st z <> x holds
(f . (s,(x /= i))) . z = s . z ) )
A1: (. (i,A,f)) . s = i by FUNCOP_1:7;
A2: (^ x) . s = x by FUNCOP_1:7;
A3: (. (^ x)) . s = s . ((^ x) . s) by Def19;
((. x) div (. (i,A,f))) . s = ((. x) . s) div ((. (i,A,f)) . s) by Def29;
hence ( (f . (s,(x /= i))) . x = (s . x) div i & ( for z being Element of X st z <> x holds
(f . (s,(x /= i))) . z = s . z ) ) by A1, A2, A3, Th24; :: thesis: verum