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 n, s, i being Variable of g st ex d being Function st
( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
for q being Element of Funcs (X,INT)
for N being Nat st N = q . n holds
(g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = 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 n, s, i being Variable of g st ex d being Function st
( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
for q being Element of Funcs (X,INT)
for N being Nat st N = q . n holds
(g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = N !
let b be Element of X; :: thesis: for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for n, s, i being Variable of g st ex d being Function st
( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
for q being Element of Funcs (X,INT)
for N being Nat st N = q . n holds
(g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = N !
let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); :: thesis: for n, s, i being Variable of g st ex d being Function st
( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
for q being Element of Funcs (X,INT)
for N being Nat st N = q . n holds
(g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = N !
set f = g;
let n, s, i be Variable of g; :: thesis: ( ex d being Function st
( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) implies for q being Element of Funcs (X,INT)
for N being Nat st N = q . n holds
(g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = N ! )
given d being Function such that A1: d . n = 1 and
A2: d . s = 2 and
A3: d . i = 3 and
A4: d . b = 4 ; :: thesis: for q being Element of Funcs (X,INT)
for N being Nat st N = q . n holds
(g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = N !
A5: ( n <> i & n <> b & i <> b ) by A1, A3, A4;
set S = Funcs (X,INT);
let q be Element of Funcs (X,INT); :: thesis: for N being Nat st N = q . n holds
(g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = N !
reconsider q1 = g . (q,(s := 1)) as Element of Funcs (X,INT) ;
defpred S1[ Element of Funcs (X,INT)] means ex K being Nat st
( K = ($1 . i) - 1 & $1 . s = K ! );
reconsider a = . (2,A,g) as INT-Expression of A,g ;
reconsider q2 = g . (q1,(i := 2)) as Element of Funcs (X,INT) ;
A6: q2 . i = 2 by Th25;
A7: s <> i by A2, A3;
then q2 . s = q1 . s by Th25;
then A8: S1[g . (q1,(i := a))] by A6, Th25, NEWTON:13;
set I = s *= i;
A10: s <> b by A2, A4;
A11: for q being Element of Funcs (X,INT) st S1[q] holds
( S1[g . (q,((s *= i) \; (i += 1)))] & S1[g . (q,(i leq n))] )
proof
let q be Element of Funcs (X,INT); :: thesis: ( S1[q] implies ( S1[g . (q,((s *= i) \; (i += 1)))] & S1[g . (q,(i leq n))] ) )
given Ki being Nat such that A12: Ki = (q . i) - 1 and
A13: q . s = Ki ! ; :: thesis: ( S1[g . (q,((s *= i) \; (i += 1)))] & S1[g . (q,(i leq n))] )
reconsider q3 = g . (q,(s *= i)) as Element of Funcs (X,INT) ;
reconsider q4 = g . (q3,(i += 1)) as Element of Funcs (X,INT) ;
A14: q3 . s = (q . s) * (q . i) by Th33;
q4 . s = q3 . s by A7, Th28;
then A15: q4 . s = (Ki + 1) ! by A12, A13, A14, NEWTON:15;
A16: q4 = g . (q,((s *= i) \; (i += 1))) by AOFA_000:def 29;
q4 . i = (q3 . i) + 1 by Th28;
then Ki + 1 = (q4 . i) - 1 by A7, A12, Th33;
hence S1[g . (q,((s *= i) \; (i += 1)))] by A16, A15; :: thesis: S1[g . (q,(i leq n))]
reconsider q9 = g . (q,(i leq n)) as Element of Funcs (X,INT) ;
q9 . i = q . i by A5, Th35;
hence S1[g . (q,(i leq n))] by A12, A13, A10, Th35; :: thesis: verum
end;
reconsider F = for-do ((i := a),(i leq n),(i += 1),(s *= i)) as Element of A ;
let N be Nat; :: thesis: ( N = q . n implies (g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = N ! )
assume A17: N = q . n ; :: thesis: (g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = N !
A18: F = for-do ((i := a),(i leq n),(i += 1),(s *= i)) ;
A19: s <> n by A1, A2;
A20: for q being Element of Funcs (X,INT) st S1[q] holds
( (g . (q,(s *= i))) . i = q . i & (g . (q,(s *= i))) . n = q . n ) by A19, A7, Th32;
A21: ( S1[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(A18, A8, A11, A20, A5);
 consider K being Nat such that
A22: K = ((g . (q1,F)) . i) - 1 and
A23: (g . (q1,F)) . s = K ! by A21;
per cases ( a . q1 <= q1 . n or a . q1 > q1 . n ) ;
suppose A24: a . q1 <= q1 . n ; :: thesis: (g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = N !
thus (g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = K ! by A23, AOFA_000:def 29
.= N ! by A17, A24, A21, A22, A19, Th25 ; :: thesis: verum
end;
suppose A25: a . q1 > q1 . n ; :: thesis: (g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = N !
then 1 + 1 > N by A19, A17, Th25;
then A26: 1 >= N by NAT_1:13;
thus (g . (q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i)))))) . s = K ! by A23, AOFA_000:def 29
.= N ! by A25, A21, A22, A26, NAT_1:25, NEWTON:12, NEWTON:13 ; :: thesis: verum
end;
end;