let I, J be Program of SCM+FSA ; :: thesis: I,J equal_outside NAT
dom I c= NAT by RELAT_1:def 18;
then (dom I) \ NAT = {} by XBOOLE_1:37;
then A1: dom (I | ((dom I) \ NAT )) = {} ;
dom J c= NAT by RELAT_1:def 18;
then (dom J) \ NAT = {} by XBOOLE_1:37;
then A2: dom (J | ((dom J) \ NAT )) = {} ;
for x being set st x in {} holds
(I | ((dom I) \ NAT )) . x = (J | ((dom J) \ NAT )) . x ;
then I | ((dom I) \ NAT ) = J | ((dom J) \ NAT ) by A1, A2, FUNCT_1:9;
hence I,J equal_outside NAT by FUNCT_7:def 2; :: thesis: verum