let k be Nat; :: thesis: for S being non empty standard-ins homogeneous J/A-independent with_halt set
for I being Element of S st IncAddr (I,k) = halt S holds
I = halt S
let S be non empty standard-ins homogeneous J/A-independent with_halt set ; :: thesis: for I being Element of S st IncAddr (I,k) = halt S holds
I = halt S
let I be Element of S; :: thesis: ( IncAddr (I,k) = halt S implies I = halt S )
assume IncAddr (I,k) = halt S ; :: thesis: I = halt S
then IncAddr (I,k) = IncAddr ((halt S),k) by Th3;
hence I = halt S by Th5; :: thesis: verum