NAT c= dom s by LmL;
hence dom (ProgramPart s) = NAT by RELAT_1:91; :: according to PARTFUN1:def 4 :: thesis: verum