let A be Euclidean preIfWhileAlgebra; :: thesis: for X being non empty countable set
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for x, n, s, i being Variable of g st ex d being Function st
( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
for q being Element of Funcs X,INT
for N being natural number st N = q . n holds
(g . q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))) . s = (q . x) |^ N
let X be non empty countable set ; :: thesis: for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for x, n, s, i being Variable of g st ex d being Function st
( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
for q being Element of Funcs X,INT
for N being natural number st N = q . n holds
(g . q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))) . s = (q . x) |^ N
let b be Element of X; :: thesis: for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for x, n, s, i being Variable of g st ex d being Function st
( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
for q being Element of Funcs X,INT
for N being natural number st N = q . n holds
(g . q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))) . s = (q . x) |^ N
let g be Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0 ; :: thesis: for x, n, s, i being Variable of g st ex d being Function st
( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
for q being Element of Funcs X,INT
for N being natural number st N = q . n holds
(g . q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))) . s = (q . x) |^ N
set f = g;
let x, n, s, i be Variable of g; :: thesis: ( ex d being Function st
( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) implies for q being Element of Funcs X,INT
for N being natural number st N = q . n holds
(g . q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))) . s = (q . x) |^ N )
given d being Function such that A1: d . x = 0 and
A2: d . n = 1 and
A3: d . s = 2 and
A4: d . i = 3 and
A5: d . b = 4 ; :: thesis: for q being Element of Funcs X,INT
for N being natural number st N = q . n holds
(g . q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))) . s = (q . x) |^ N
A6: ( n <> i & n <> b & i <> b ) by A2, A4, A5;
set S = Funcs X,INT ;
let q be Element of Funcs X,INT ; :: thesis: for N being natural number st N = q . n holds
(g . q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))) . s = (q . x) |^ N
reconsider q1 = g . q,(s := 1) as Element of Funcs X,INT ;
reconsider q2 = g . q1,(i := 1) as Element of Funcs X,INT ;
A7: s <> i by A3, A4;
then A8: q2 . s = q1 . s by Th25;
defpred S₁[ Element of Funcs X,INT ] means ex K being natural number st
( K = ($1 . i) - 1 & $1 . s = (q . x) |^ K & $1 . x = q . x );
set I = s *= x;
set q0 = q;
A9: (q . x) |^ 0 = 1 by NEWTON:9;
A10: s <> n by A2, A3;
then A11: for q being Element of Funcs X,INT st S₁[q] holds
( (g . q,(s *= x)) . i = q . i & (g . q,(s *= x)) . n = q . n ) by A7, Th32;
A12: s <> b by A3, A5;
A13: for q being Element of Funcs X,INT st S₁[q] holds
( S₁[g . q,((s *= x) \; (i += 1))] & S₁[g . q,(i leq n)] )

proof

let q be Element of Funcs X,INT ; :: thesis: ( S₁[q] implies ( S₁[g . q,((s *= x) \; (i += 1))] & S₁[g . q,(i leq n)] ) )
given Ki being natural number such that A14: Ki = (q . i) - 1 and
A15: q . s = (q . x) |^ Ki and
A16: q . x = q . x ; :: thesis: ( S₁[g . q,((s *= x) \; (i += 1))] & S₁[g . q,(i leq n)] )
reconsider q3 = g . q,(s *= x) as Element of Funcs X,INT ;
reconsider q4 = g . q3,(i += 1) as Element of Funcs X,INT ;
A17: q3 . s = (q . s) * (q . x) by Th33;
q4 . s = q3 . s by A7, Th28;
then A18: q4 . s = (q . x) |^ (Ki + 1) by A15, A16, A17, NEWTON:11;
A19: q4 = g . q,((s *= x) \; (i += 1)) by AOFA_000:def 29;
A20: q3 . x = q . x by A1, A3, Th33;
q4 . i = (q3 . i) + 1 by Th28;
then Ki + 1 = (q4 . i) - 1 by A7, A14, Th33;
hence S₁[g . q,((s *= x) \; (i += 1))] by A1, A4, A16, A19, A20, A18, Th28; :: thesis: S₁[g . q,(i leq n)]
reconsider q9 = g . q,(i leq n) as Element of Funcs X,INT ;
A21: q9 . s = q . s by A12, Th35;
A22: q9 . i = q . i by A6, Th35;
q9 . x = q . x by A1, A5, Th35;
hence S₁[g . q,(i leq n)] by A14, A15, A16, A21, A22; :: thesis: verum

end;

reconsider a = . 1,A,g as INT-Expression of A,g ;
reconsider F = for-do (i := a),(i leq n),(i += 1),(s *= x) as Element of A ;
A23: F = for-do (i := a),(i leq n),(i += 1),(s *= x) ;
A24: q2 . i = 1 by Th25;
A25: q2 . x = q1 . x by A1, A4, Th25;
A26: q1 . s = 1 by Th25;
q1 . x = q . x by A1, A3, Th25;
then A27: S₁[g . q1,(i := a)] by A26, A8, A24, A25, A9;
A28: ( S₁[g . q1,F] & ( a . q1 <= q1 . n implies (g . q1,F) . i = (q1 . n) + 1 ) & ( a . q1 > q1 . n implies (g . q1,F) . i = a . q1 ) & (g . q1,F) . n = q1 . n ) from AOFA_I00:sch 1(A23, A27, A13, A11, A6);
A29: ((q . n) + 1) - 1 = q . n ;
A30: q1 . n = q . n by A10, Th25;
set T = (Funcs X,INT ) \ b,0 ;
let N be natural number ; :: thesis: ( N = q . n implies (g . q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))) . s = (q . x) |^ N )
assume A31: N = q . n ; :: thesis: (g . q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))) . s = (q . x) |^ N
A32: ( N = 0 or N >= 1 ) by NAT_1:26;
thus (g . q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))) . s = (g . q1,F) . s by AOFA_000:def 29
.= (q . x) |^ N by A31, A30, A29, A28, A32, FUNCOP_1:13 ; :: thesis: verum