A: dom (Start-At (0,S)) misses NAT by Th26;
B: dom p misses NAT by Lm40;
dom (Initialize p) = (dom (Start-At (0,S))) \/ (dom p) by FUNCT_4:def 1;
then dom (Initialize p) misses NAT by A, B, XBOOLE_1:70;
hence (Initialize p) | NAT = {} by RELAT_1:95; :: according to COMPOS_1:def 29 :: thesis: verum