let n be Nat; :: thesis: for P being IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM
for s being 0 -started State-consisting of <%1,n,1%> holds
( ( for k being Nat st k < n holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = (n !) / (((Comput (P,s,((4 * k) + 1))) . (dl. 1)) !) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = (n !) / ((((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1) !) & (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) ) ) & ( for k, j being Nat st k >= n holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = n ! ) & (Result (P,s)) . (dl. 2) = n ! )
let P be IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM; :: thesis: for s being 0 -started State-consisting of <%1,n,1%> holds
( ( for k being Nat st k < n holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = (n !) / (((Comput (P,s,((4 * k) + 1))) . (dl. 1)) !) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = (n !) / ((((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1) !) & (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) ) ) & ( for k, j being Nat st k >= n holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = n ! ) & (Result (P,s)) . (dl. 2) = n ! )
let s be 0 -started State-consisting of <%1,n,1%>; :: thesis: ( ( for k being Nat st k < n holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = (n !) / (((Comput (P,s,((4 * k) + 1))) . (dl. 1)) !) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = (n !) / ((((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1) !) & (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) ) ) & ( for k, j being Nat st k >= n holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = n ! ) & (Result (P,s)) . (dl. 2) = n ! )
A1: H₂( 0 ) = 1 by NEWTON:12;
A2: 1 <> 0 ;
A3: for n being Nat holds H₂(n + 1) = (n + 1) * H₂(n) by NEWTON:15;
A4: for P being IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM
for s being 0 -started State-consisting of <%1,n,1%> holds
( ( for k being Nat st k < n holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = 1 * (H₂(n) / H₂((Comput (P,s,((4 * k) + 1))) . (dl. 1))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = 1 * (H₂(n) / H₂(((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1)) & (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) ) ) & ( for k, j being Nat st k >= n holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = H₂(n) ) & (Result (P,s)) . (dl. 2) = H₂(n) ) from AMI_8:sch 2(A1, A2, A3);

hereby :: thesis: ( ( for k, j being Nat st k >= n holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = n ! ) & (Result (P,s)) . (dl. 2) = n ! )

let k be Nat; :: thesis: ( k < n implies ( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = H₂(n) / H₂((Comput (P,s,((4 * k) + 1))) . (dl. 1)) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = H₂(n) / H₂(((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1) & (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) ) )
assume A5: k < n ; :: thesis: ( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = H₂(n) / H₂((Comput (P,s,((4 * k) + 1))) . (dl. 1)) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = H₂(n) / H₂(((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1) & (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) )
thus (Comput (P,s,((4 * k) + 1))) . (dl. 2) = 1 * (H₂(n) / H₂((Comput (P,s,((4 * k) + 1))) . (dl. 1))) by A4, A5
.= H₂(n) / H₂((Comput (P,s,((4 * k) + 1))) . (dl. 1)) ; :: thesis: ( (Comput (P,s,((4 * k) + 2))) . (dl. 2) = H₂(n) / H₂(((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1) & (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) )
thus (Comput (P,s,((4 * k) + 2))) . (dl. 2) = 1 * (H₂(n) / H₂(((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1)) by A4, A5
.= H₂(n) / H₂(((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1) ; :: thesis: ( (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) )
thus (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) by A4, A5; :: thesis: (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2)
thus (Comput (P,s,((4 * k) + 4))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) by A4, A5; :: thesis: verum

end;

thus ( ( for k, j being Nat st k >= n holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = n ! ) & (Result (P,s)) . (dl. 2) = n ! ) by A4; :: thesis: verum