let IT1, IT2 be Element of NAT ; :: thesis: ( ( F is halting & F . IT1 = F . (IT1 + 1) & ( for n being Nat st F . n = F . (n + 1) holds
IT1 <= n ) & F . IT2 = F . (IT2 + 1) & ( for n being Nat st F . n = F . (n + 1) holds
IT2 <= n ) implies IT1 = IT2 ) & ( not F is halting & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) )
hereby :: thesis: ( not F is halting & IT1 = 0 & IT2 = 0 implies IT1 = IT2 )
assume F is halting ; :: thesis: ( F . IT1 = F . (IT1 + 1) & ( for n being Nat st F . n = F . (n + 1) holds
IT1 <= n ) & F . IT2 = F . (IT2 + 1) & ( for n being Nat st F . n = F . (n + 1) holds
IT2 <= n ) implies IT1 = IT2 )
assume A3: ( F . IT1 = F . (IT1 + 1) & ( for n being Nat st F . n = F . (n + 1) holds
IT1 <= n ) ) ; :: thesis: ( F . IT2 = F . (IT2 + 1) & ( for n being Nat st F . n = F . (n + 1) holds
IT2 <= n ) implies IT1 = IT2 )
assume ( F . IT2 = F . (IT2 + 1) & ( for n being Nat st F . n = F . (n + 1) holds
IT2 <= n ) ) ; :: thesis: IT1 = IT2
then ( IT1 <= IT2 & IT2 <= IT1 ) by A3;
hence IT1 = IT2 by XXREAL_0:1; :: thesis: verum
end;
thus ( not F is halting & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) ; :: thesis: verum