let P be IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM; :: thesis: for s being 0 -started State-consisting of <%1,F₂(),F₁()%> holds
( ( for k being Nat st k < F₂() holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * k) + 1))) . (dl. 1)))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((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 >= F₂() holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = F₃(F₂()) ) & (Result (P,s)) . (dl. 2) = F₃(F₂()) )
A4: IterativeAlgorithm (MultBy ((dl. 2),(dl. 1))) c= P by PROOFS_1:def 12;
let s be 0 -started State-consisting of <%1,F₂(),F₁()%>; :: thesis: ( ( for k being Nat st k < F₂() holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * k) + 1))) . (dl. 1)))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((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 >= F₂() holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = F₃(F₂()) ) & (Result (P,s)) . (dl. 2) = F₃(F₂()) )
A5: P . 1 = halt SCM by A4, Th8;
set s0 = Comput (P,s,0);
set s1 = Comput (P,s,(0 + 1));
set s2 = Comput (P,s,(1 + 1));
set s3 = Comput (P,s,(2 + 1));
set s4 = Comput (P,s,(3 + 1));
set s5 = Comput (P,s,(4 + 1));
A6: IC (Comput (P,s,0)) = 0 by MEMSTR_0:def 12;
A7: (Comput (P,s,0)) . (dl. 1) = F₂() by Th14;
A8: (Comput (P,s,0)) . (dl. 2) = F₁() by Th14;
A9: (Comput (P,s,(0 + 1))) . (dl. 1) = (Comput (P,s,0)) . (dl. 1) by A4, A6, Th16;
A10: (Comput (P,s,(0 + 1))) . (dl. 2) = (Comput (P,s,0)) . (dl. 2) by A4, A6, Th16;

per cases ( F₂() = 0 or ex K being Nat st F₂() = K + 1 ) by NAT_1:6;

suppose A11: F₂() = 0 ; :: thesis: ( ( for k being Nat st k < F₂() holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * k) + 1))) . (dl. 1)))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((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 >= F₂() holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = F₃(F₂()) ) & (Result (P,s)) . (dl. 2) = F₃(F₂()) )

then A12: P . (IC (Comput (P,s,(0 + 1)))) = halt SCM by A5, A4, A6, A7, Th16;
thus for k being Nat st k < F₂() holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * k) + 1))) . (dl. 1)))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((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) ) by A11; :: thesis: ( ( for k, j being Nat st k >= F₂() holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = F₃(F₂()) ) & (Result (P,s)) . (dl. 2) = F₃(F₂()) )
defpred S₁[ Nat] means for j being Nat st $1 >= F₂() holds
(Comput (P,s,(((4 * $1) + 1) + j))) . (dl. 2) = F₃(F₂());
A13: S₁[ 0 ]

proof

let j be Nat; :: thesis: ( 0 >= F₂() implies (Comput (P,s,(((4 * 0) + 1) + j))) . (dl. 2) = F₃(F₂()) )
assume A14: 0 >= F₂() ; :: thesis: (Comput (P,s,(((4 * 0) + 1) + j))) . (dl. 2) = F₃(F₂())
A15: F₂() = 0 by A14;
defpred S₂[ Nat] means (Comput (P,s,(((4 * 0) + 1) + $1))) . (dl. 2) = F₃(F₂());
A16: S₂[ 0 ] by A1, A8, A10, A14;
A17: for h being Nat st S₂[h] holds
S₂[h + 1]

proof

let h be Nat; :: thesis: ( S₂[h] implies S₂[h + 1] )
assume A18: S₂[h] ; :: thesis: S₂[h + 1]
1 <= h + 1 by NAT_1:11;
then IC (Comput (P,s,(h + 1))) = 1 by A4, A15, Th27;
hence (Comput (P,s,(((4 * 0) + 1) + (h + 1)))) . (dl. 2) = F₃(F₂()) by A4, A18, Th18; :: thesis: verum

end;

for h being Nat holds S₂[h] from NAT_1:sch 2(A16, A17);
hence (Comput (P,s,(((4 * 0) + 1) + j))) . (dl. 2) = F₃(F₂()) ; :: thesis: verum

end;

A19: for z being Nat st S₁[z] holds
S₁[z + 1]

proof

let z be Nat; :: thesis: ( S₁[z] implies S₁[z + 1] )
assume A20: S₁[z] ; :: thesis: S₁[z + 1]
let j be Nat; :: thesis: ( z + 1 >= F₂() implies (Comput (P,s,(((4 * (z + 1)) + 1) + j))) . (dl. 2) = F₃(F₂()) )
assume z + 1 >= F₂() ; :: thesis: (Comput (P,s,(((4 * (z + 1)) + 1) + j))) . (dl. 2) = F₃(F₂())
(Comput (P,s,(((4 * z) + 1) + (j + 4)))) . (dl. 2) = F₃(F₂()) by A11, A20;
hence (Comput (P,s,(((4 * (z + 1)) + 1) + j))) . (dl. 2) = F₃(F₂()) ; :: thesis: verum

end;

for z being Nat holds S₁[z] from NAT_1:sch 2(A13, A19);
hence for k, j being Nat st k >= F₂() holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = F₃(F₂()) ; :: thesis: (Result (P,s)) . (dl. 2) = F₃(F₂())
thus (Result (P,s)) . (dl. 2) = F₃(F₂()) by A1, A8, A10, A11, A12, EXTPRO_1:7; :: thesis: verum

end;

suppose ex K being Nat st F₂() = K + 1 ; :: thesis: ( ( for k being Nat st k < F₂() holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * k) + 1))) . (dl. 1)))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((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 >= F₂() holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = F₃(F₂()) ) & (Result (P,s)) . (dl. 2) = F₃(F₂()) )

then consider K being Nat such that
A21: F₂() = K + 1 ;
A22: IC (Comput (P,s,(0 + 1))) = 2 by A4, A6, A7, A21, Th16;
A23: IC (Comput (P,s,(1 + 1))) = 3 by A4, A22, Th21;
A24: (Comput (P,s,(1 + 1))) . (dl. 2) = ((Comput (P,s,(0 + 1))) . (dl. 2)) * ((Comput (P,s,(0 + 1))) . (dl. 1)) by A4, A22, Th21;
A25: IC (Comput (P,s,(2 + 1))) = 4 by A4, A23, Th22;
A26: (Comput (P,s,(2 + 1))) . (dl. 2) = (Comput (P,s,(1 + 1))) . (dl. 2) by A4, A23, Th22;
A27: (Comput (P,s,(3 + 1))) . (dl. 2) = (Comput (P,s,(2 + 1))) . (dl. 2) by A4, A25, Th23;
defpred S₁[ Nat] means ( ( $1 < F₂() implies ( (Comput (P,s,((4 * $1) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * $1) + 1))) . (dl. 1)))) & (Comput (P,s,((4 * $1) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((Comput (P,s,((4 * $1) + 2))) . (dl. 1)) -' 1))) & (Comput (P,s,((4 * $1) + 3))) . (dl. 2) = (Comput (P,s,((4 * $1) + 2))) . (dl. 2) & (Comput (P,s,((4 * $1) + 4))) . (dl. 2) = (Comput (P,s,((4 * $1) + 3))) . (dl. 2) ) ) & ( for j being Nat st $1 >= F₂() holds
(Comput (P,s,(((4 * $1) + 1) + j))) . (dl. 2) = F₃(F₂()) ) );
A28: S₁[ 0 ]

proof

hereby :: thesis: for j being Nat st 0 >= F₂() holds
(Comput (P,s,(((4 * 0) + 1) + j))) . (dl. 2) = F₃(F₂())

assume 0 < F₂() ; :: thesis: ( (Comput (P,s,((4 * 0) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * 0) + 1))) . (dl. 1)))) & (Comput (P,s,((4 * 0) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((Comput (P,s,((4 * 0) + 2))) . (dl. 1)) -' 1))) & (Comput (P,s,((4 * 0) + 3))) . (dl. 2) = (Comput (P,s,((4 * 0) + 2))) . (dl. 2) & (Comput (P,s,((4 * 0) + 4))) . (dl. 2) = (Comput (P,s,((4 * 0) + 3))) . (dl. 2) )
then consider k being Nat such that
A29: F₂() = k + 1 by NAT_1:6;
A30: F₃((k + 1)) = (k + 1) * F₃(k) by A3;
A31: for n being Nat holds F₃(n) <> 0

proof

defpred S₂[ Nat] means F₃($1) <> 0 ;
A32: S₂[ 0 ] by A1, A2;
A33: for z being Nat st S₂[z] holds
S₂[z + 1]

proof

let z be Nat; :: thesis: ( S₂[z] implies S₂[z + 1] )
F₃((z + 1)) = (z + 1) * F₃(z) by A3;
hence ( S₂[z] implies S₂[z + 1] ) by XCMPLX_1:6; :: thesis: verum

end;

for z being Nat holds S₂[z] from NAT_1:sch 2(A32, A33);
hence for n being Nat holds F₃(n) <> 0 ; :: thesis: verum

end;

thus (Comput (P,s,((4 * 0) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * 0) + 1))) . (dl. 1)))) by A7, A8, A9, A10, A31, XCMPLX_1:88; :: thesis: ( (Comput (P,s,((4 * 0) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((Comput (P,s,((4 * 0) + 2))) . (dl. 1)) -' 1))) & (Comput (P,s,((4 * 0) + 3))) . (dl. 2) = (Comput (P,s,((4 * 0) + 2))) . (dl. 2) & (Comput (P,s,((4 * 0) + 4))) . (dl. 2) = (Comput (P,s,((4 * 0) + 3))) . (dl. 2) )
A34: (Comput (P,s,((4 * 0) + 2))) . (dl. 1) = F₂() - 0 by A4, A29, Th29;
then 0 + 1 <= (Comput (P,s,((4 * 0) + 2))) . (dl. 1) by A29, NAT_1:13;
then ((Comput (P,s,((4 * 0) + 2))) . (dl. 1)) -' 1 = ((Comput (P,s,((4 * 0) + 2))) . (dl. 1)) - 1 by XREAL_1:233;
hence (Comput (P,s,((4 * 0) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((Comput (P,s,((4 * 0) + 2))) . (dl. 1)) -' 1))) by A7, A8, A29, A9, A10, A24, A30, A31, A34, XCMPLX_1:89; :: thesis: ( (Comput (P,s,((4 * 0) + 3))) . (dl. 2) = (Comput (P,s,((4 * 0) + 2))) . (dl. 2) & (Comput (P,s,((4 * 0) + 4))) . (dl. 2) = (Comput (P,s,((4 * 0) + 3))) . (dl. 2) )
thus (Comput (P,s,((4 * 0) + 3))) . (dl. 2) = (Comput (P,s,((4 * 0) + 2))) . (dl. 2) by A26; :: thesis: (Comput (P,s,((4 * 0) + 4))) . (dl. 2) = (Comput (P,s,((4 * 0) + 3))) . (dl. 2)
thus (Comput (P,s,((4 * 0) + 4))) . (dl. 2) = (Comput (P,s,((4 * 0) + 3))) . (dl. 2) by A27; :: thesis: verum

end;

thus for j being Nat st 0 >= F₂() holds
(Comput (P,s,(((4 * 0) + 1) + j))) . (dl. 2) = F₃(F₂()) by A21; :: thesis: verum

end;

A35: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A36: ( ( k < F₂() implies ( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * k) + 1))) . (dl. 1)))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((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 j being Nat st k >= F₂() holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = F₃(F₂()) ) ) ; :: thesis: S₁[k + 1]
set t = Comput (P,s,((4 * k) + 2));
set S = (4 * k) + 3;
set s3 = Comput (P,s,((4 * k) + 3));
set s4 = Comput (P,s,(((4 * k) + 3) + 1));
set s5 = Comput (P,s,((((4 * k) + 3) + 1) + 1));
set s6 = Comput (P,s,((((4 * k) + 3) + 2) + 1));
set s7 = Comput (P,s,((((4 * k) + 3) + 3) + 1));
set s8 = Comput (P,s,((((4 * k) + 3) + 4) + 1));

hereby :: thesis: for j being Nat st k + 1 >= F₂() holds
(Comput (P,s,(((4 * (k + 1)) + 1) + j))) . (dl. 2) = F₃(F₂())

assume A37: k + 1 < F₂() ; :: thesis: ( (Comput (P,s,((4 * (k + 1)) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * (k + 1)) + 1))) . (dl. 1)))) & (Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 1)) -' 1))) & (Comput (P,s,((4 * (k + 1)) + 3))) . (dl. 2) = (Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 2) & (Comput (P,s,((4 * (k + 1)) + 4))) . (dl. 2) = (Comput (P,s,((4 * (k + 1)) + 3))) . (dl. 2) )
then A38: k < F₂() by XXREAL_0:2, NAT_1:16;
A39: F₂() - (k + 1) > (k + 1) - (k + 1) by A37, XREAL_1:9;
A40: IC (Comput (P,s,((4 * k) + 3))) = 4 by A4, A38, Th29;
A41: (Comput (P,s,((4 * k) + 3))) . (dl. 1) = (F₂() - k) - 1 by A4, A38, Th29;
then A42: IC (Comput (P,s,(((4 * k) + 3) + 1))) = 5 by A4, A39, A40, Th23;
then A43: IC (Comput (P,s,((((4 * k) + 3) + 1) + 1))) = 2 by A4, Th24;
A44: (Comput (P,s,(((4 * k) + 3) + 1))) . (dl. 1) = (Comput (P,s,((4 * k) + 3))) . (dl. 1) by A4, A40, Th23;
A45: (Comput (P,s,((((4 * k) + 3) + 1) + 1))) . (dl. 1) = (Comput (P,s,(((4 * k) + 3) + 1))) . (dl. 1) by A4, A42, Th24;
A46: IC (Comput (P,s,((((4 * k) + 3) + 2) + 1))) = 3 by A4, A43, Th21;
A47: (Comput (P,s,((4 * k) + 3))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1))) by A36, A38;
A48: (Comput (P,s,(((4 * k) + 3) + 1))) . (dl. 2) = (Comput (P,s,((4 * k) + 3))) . (dl. 2) by A4, A40, Th23;
A49: (Comput (P,s,((((4 * k) + 3) + 1) + 1))) . (dl. 2) = (Comput (P,s,(((4 * k) + 3) + 1))) . (dl. 2) by A4, A42, Th24;
A50: (Comput (P,s,((((4 * k) + 3) + 2) + 1))) . (dl. 2) = ((Comput (P,s,((((4 * k) + 3) + 1) + 1))) . (dl. 2)) * ((Comput (P,s,((((4 * k) + 3) + 1) + 1))) . (dl. 1)) by A4, A43, Th21;
A51: (Comput (P,s,((((4 * k) + 3) + 3) + 1))) . (dl. 2) = (Comput (P,s,((((4 * k) + 3) + 2) + 1))) . (dl. 2) by A4, A46, Th22;
((F₂() - k) - 1) - 1 >= 0 by A39, INT_1:52;
then reconsider W = (F₂() - k) - 2 as Element of NAT by INT_1:3;
F₃((W + 1)) = (W + 1) * F₃(W) by A3;
then A52: F₃(F₂()) / F₃(W) = F₃(F₂()) / (F₃(((F₂() - k) - 1)) / ((F₂() - k) - 1)) by XCMPLX_1:89
.= (F₃(F₂()) * ((F₂() - k) - 1)) / F₃(((F₂() - k) - 1)) by XCMPLX_1:77 ;
A53: (Comput (P,s,((4 * k) + 2))) . (dl. 1) = F₂() - k by A4, A38, Th29;
then 0 + 1 <= (Comput (P,s,((4 * k) + 2))) . (dl. 1) by A38, NAT_1:13, XREAL_1:50;
then A54: ((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1 = ((Comput (P,s,((4 * k) + 2))) . (dl. 1)) - 1 by XREAL_1:233;
hence (Comput (P,s,((4 * (k + 1)) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * (k + 1)) + 1))) . (dl. 1)))) by A44, A45, A41, A36, A38, A49, A53; :: thesis: ( (Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 1)) -' 1))) & (Comput (P,s,((4 * (k + 1)) + 3))) . (dl. 2) = (Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 2) & (Comput (P,s,((4 * (k + 1)) + 4))) . (dl. 2) = (Comput (P,s,((4 * (k + 1)) + 3))) . (dl. 2) )
A55: (Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 1) = F₂() - (k + 1) by A4, A37, Th29;
then 0 + 1 <= (Comput (P,s,((((4 * k) + 3) + 2) + 1))) . (dl. 1) by A39, NAT_1:13;
then ((Comput (P,s,((((4 * k) + 3) + 2) + 1))) . (dl. 1)) -' 1 = ((Comput (P,s,((((4 * k) + 3) + 2) + 1))) . (dl. 1)) - 1 by XREAL_1:233;
then A56: (F₃(F₂()) / F₃((((Comput (P,s,((4 * k) + 2))) . (dl. 1)) - 1))) * ((F₂() - k) - 1) = F₃(F₂()) / F₃((((Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 1)) -' 1)) by A52, A53, A55;
thus (Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 1)) -' 1))) by A41, A47, A44, A45, A48, A49, A50, A54, A56; :: thesis: ( (Comput (P,s,((4 * (k + 1)) + 3))) . (dl. 2) = (Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 2) & (Comput (P,s,((4 * (k + 1)) + 4))) . (dl. 2) = (Comput (P,s,((4 * (k + 1)) + 3))) . (dl. 2) )
thus (Comput (P,s,((4 * (k + 1)) + 3))) . (dl. 2) = (Comput (P,s,((4 * (k + 1)) + 2))) . (dl. 2) by A51; :: thesis: (Comput (P,s,((4 * (k + 1)) + 4))) . (dl. 2) = (Comput (P,s,((4 * (k + 1)) + 3))) . (dl. 2)
A57: ((4 * (k + 1)) + 3) + 1 = (4 * (k + 1)) + 4 ;
IC (Comput (P,s,((4 * (k + 1)) + 3))) = 4 by A4, A37, Th29;
hence (Comput (P,s,((4 * (k + 1)) + 4))) . (dl. 2) = (Comput (P,s,((4 * (k + 1)) + 3))) . (dl. 2) by A4, A57, Th23; :: thesis: verum

end;

let j be Nat; :: thesis: ( k + 1 >= F₂() implies (Comput (P,s,(((4 * (k + 1)) + 1) + j))) . (dl. 2) = F₃(F₂()) )
assume k + 1 >= F₂() ; :: thesis: (Comput (P,s,(((4 * (k + 1)) + 1) + j))) . (dl. 2) = F₃(F₂())

per cases then ( k + 1 = F₂() or k + 1 > F₂() ) by XXREAL_0:1;

suppose A58: k + 1 = F₂() ; :: thesis: (Comput (P,s,(((4 * (k + 1)) + 1) + j))) . (dl. 2) = F₃(F₂())

A59: k < k + 1 by NAT_1:16;
then A60: (Comput (P,s,((4 * k) + 2))) . (dl. 1) = F₂() - k by A4, A58, Th29
.= 1 by A58 ;
then ((Comput (P,s,((4 * k) + 2))) . (dl. 1)) -' 1 = ((Comput (P,s,((4 * k) + 2))) . (dl. 1)) - 1 by XREAL_1:233;
then A61: (Comput (P,s,((4 * k) + 3))) . (dl. 2) = (F₁() * F₃(F₂())) / F₁() by A1, A36, A58, A59, A60
.= F₃(F₂()) by A2, XCMPLX_1:89 ;
A62: IC (Comput (P,s,((4 * k) + 3))) = 4 by A4, A58, A59, Th29;
(Comput (P,s,((4 * k) + 3))) . (dl. 1) = (F₂() - k) - 1 by A4, A58, A59, Th29
.= 0 by A58 ;
then IC (Comput (P,s,(((4 * k) + 3) + 1))) = 1 by A4, A62, Th23;
then Comput (P,s,(((4 * k) + 4) + (j + 1))) = Comput (P,s,(((4 * k) + 3) + 1)) by A4, Th18;
hence (Comput (P,s,(((4 * (k + 1)) + 1) + j))) . (dl. 2) = F₃(F₂()) by A61, A4, A62, Th23; :: thesis: verum

end;

suppose k + 1 > F₂() ; :: thesis: (Comput (P,s,(((4 * (k + 1)) + 1) + j))) . (dl. 2) = F₃(F₂())

then (Comput (P,s,(((4 * k) + 1) + (j + 4)))) . (dl. 2) = F₃(F₂()) by A36, NAT_1:13;
hence (Comput (P,s,(((4 * (k + 1)) + 1) + j))) . (dl. 2) = F₃(F₂()) ; :: thesis: verum

end;

end;

end;

A63: for k being Nat holds S₁[k] from NAT_1:sch 2(A28, A35);
set t2 = Comput (P,s,((4 * K) + 2));
set t3 = Comput (P,s,((4 * K) + 3));
set t4 = Comput (P,s,(((4 * K) + 3) + 1));
A64: K < F₂() by A21, NAT_1:13;
then A65: IC (Comput (P,s,((4 * K) + 3))) = 4 by A4, Th29;
(Comput (P,s,((4 * K) + 3))) . (dl. 1) = (F₂() - K) - 1 by A4, A64, Th29
.= 0 by A21 ;
then A66: IC (Comput (P,s,(((4 * K) + 3) + 1))) = 1 by A4, A65, Th23;
A67: (Comput (P,s,((4 * K) + 2))) . (dl. 1) = F₂() - K by A4, A64, Th29;
then A68: ((Comput (P,s,((4 * K) + 2))) . (dl. 1)) -' 1 = ((Comput (P,s,((4 * K) + 2))) . (dl. 1)) - 1 by A21, XREAL_1:233;
A69: (Comput (P,s,((4 * K) + 3))) . (dl. 2) = (Comput (P,s,((4 * K) + 2))) . (dl. 2) by A63, A64
.= F₁() * (F₃(F₂()) / F₃((((Comput (P,s,((4 * K) + 2))) . (dl. 1)) -' 1))) by A63, A64
.= F₃((K + 1)) by A1, A2, A21, A67, A68, XCMPLX_1:87 ;
thus for k being Nat st k < F₂() holds
( (Comput (P,s,((4 * k) + 1))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃(((Comput (P,s,((4 * k) + 1))) . (dl. 1)))) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = F₁() * (F₃(F₂()) / F₃((((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) ) by A63; :: thesis: ( ( for k, j being Nat st k >= F₂() holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = F₃(F₂()) ) & (Result (P,s)) . (dl. 2) = F₃(F₂()) )
thus for k, j being Nat st k >= F₂() holds
(Comput (P,s,(((4 * k) + 1) + j))) . (dl. 2) = F₃(F₂()) by A63; :: thesis: (Result (P,s)) . (dl. 2) = F₃(F₂())
(Comput (P,s,(((4 * K) + 3) + 1))) . (dl. 2) = (Comput (P,s,((4 * K) + 3))) . (dl. 2) by A4, A65, Th23;
hence (Result (P,s)) . (dl. 2) = F₃(F₂()) by A5, A21, A69, A66, EXTPRO_1:7; :: thesis: verum

end;

end;