thus ( s halts_at l implies s . l = halt S ) ; :: thesis: ( s . l = halt S implies s halts_at l )
assume A1: s . l = halt S ; :: thesis: s halts_at l
l in NAT by ORDINAL1:def 12;
hence l in dom s by PARTFUN1:def 2; :: according to COMPOS_1:def 12 :: thesis: s . l = halt S
thus s . l = halt S by A1; :: thesis: verum