thus ( s halts_at l implies s . l = halt S ) by Def42; :: thesis: ( s . l = halt S implies s halts_at l )
assume Z: s . l = halt S ; :: thesis: s halts_at l
A: l in NAT by ORDINAL1:def 13;
NAT = dom s by PARTFUN1:def 4;
hence l in dom s by A; :: according to COMPOS_1:def 19 :: thesis: s . l = halt S
thus s . l = halt S by Z; :: thesis: verum