deffunc H1( Nat, set ) -> Element of NAT = IFEQ ($2,0,0,F2($1));
consider q being sequence of NAT such that
A6: q . 0 = F3() and
A7: for i being Nat holds q . (i + 1) = H1(i,q . i) from NAT_1:sch 12();
 deffunc H2( Nat) -> Element of NAT = q . $1;
q . (0 + 1) = IFEQ ((q . 0),0,0,F2(0)) by A7
.= F2(0) by A2, A6, FUNCOP_1:def 8 ;
then A8: ( H2( 0 ) = F3() & H2(1) = F4() ) by A4, A6;
A9: for k being Nat st q . k > 0 holds
q . k = F1(k)
proof
let k be Nat; :: thesis: ( q . k > 0 implies q . k = F1(k) )
assume A10: q . k > 0 ; :: thesis: q . k = F1(k)
now :: thesis: ( ( k = 0 & q . k = F1(k) ) or ( k <> 0 & q . k = F1(k) ) )
per cases ( k = 0 or k <> 0 ) ;
case k = 0 ; :: thesis: q . k = F1(k)
hence q . k = F1(k) by A3, A6; :: thesis: verum
end;
case k <> 0 ; :: thesis: q . k = F1(k)
then consider i being Nat such that
A11: k = i + 1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A12: now :: thesis: not q . i = 0
assume A13: q . i = 0 ; :: thesis: contradiction
q . k = IFEQ ((q . i),0,0,F2(i)) by A7, A11
.= 0 by A13, FUNCOP_1:def 8 ;
hence contradiction by A10; :: thesis: verum
end;
q . k = IFEQ ((q . i),0,0,F2(i)) by A7, A11
.= F2(i) by A12, FUNCOP_1:def 8 ;
hence q . k = F1(k) by A5, A10, A11; :: thesis: verum
end;
end;
end;
hence q . k = F1(k) ; :: thesis: verum
end;
A14: for k being Nat holds H2(k + 2) = H2(k) mod H2(k + 1)
proof
let k be Nat; :: thesis: H2(k + 2) = H2(k) mod H2(k + 1)
now :: thesis: ( ( q . (k + 1) <> 0 & H2(k + 2) = H2(k) mod H2(k + 1) ) or ( q . (k + 1) = 0 & q . (k + 2) = (q . k) mod (q . (k + 1)) ) )
per cases ( q . (k + 1) <> 0 or q . (k + 1) = 0 ) ;
case A15: q . (k + 1) <> 0 ; :: thesis: H2(k + 2) = H2(k) mod H2(k + 1)
A16: now :: thesis: not F2(k) = 0
A17: ( q . k = 0 or q . k <> 0 ) ;
assume A18: F2(k) = 0 ; :: thesis: contradiction
q . (k + 1) = IFEQ ((q . k),0,0,F2(k)) by A7
.= 0 by A18, A17, FUNCOP_1:def 8 ;
hence contradiction by A15; :: thesis: verum
end;
A19: q . (k + (1 + 1)) = q . ((k + 1) + 1)
.= IFEQ ((q . (k + 1)),0,0,F2((k + 1))) by A7
.= F2((k + 1)) by A15, FUNCOP_1:def 8
.= F1(k) mod F2(k) by A5, A16 ;
A20: now :: thesis: not q . k = 0
assume A21: q . k = 0 ; :: thesis: contradiction
q . (k + 1) = IFEQ ((q . k),0,0,F2(k)) by A7
.= 0 by A21, FUNCOP_1:def 8 ;
hence contradiction by A15; :: thesis: verum
end;
q . (k + 1) = IFEQ ((q . k),0,0,F2(k)) by A7
.= F2(k) by A20, FUNCOP_1:def 8 ;
hence H2(k + 2) = H2(k) mod H2(k + 1) by A9, A19, A20; :: thesis: verum
end;
case A22: q . (k + 1) = 0 ; :: thesis: q . (k + 2) = (q . k) mod (q . (k + 1))
thus q . (k + 2) = q . ((k + 1) + 1)
.= IFEQ ((q . (k + 1)),0,0,F2((k + 1))) by A7
.= 0 by A22, FUNCOP_1:def 8
.= (q . k) mod (q . (k + 1)) by A22, NAT_D:def 2 ; :: thesis: verum
end;
end;
end;
hence H2(k + 2) = H2(k) mod H2(k + 1) ; :: thesis: verum
end;
A23: ( 0 < F4() & F4() < F3() ) by A1, A2;
consider k being Nat such that
A24: ( H2(k) = F3() gcd F4() & H2(k + 1) = 0 ) from NAT_D:sch 1(A23, A8, A14);
 take k ; :: thesis: ( F1(k) = F3() gcd F4() & F2(k) = 0 )
thus F1(k) = F3() gcd F4() by A1, A9, A24, Th58; :: thesis: F2(k) = 0
F3() gcd F4() > 0 by A1, Th58;
hence F2(k) = IFEQ ((q . k),0,0,F2(k)) by A24, FUNCOP_1:def 8
.= 0 by A7, A24 ;
:: thesis: verum