let I be non empty Program of SCM+FSA; :: thesis: 0 in dom (Initialized I)
A2: 0 in dom I by AFINSQ_1:69;
I c= Initialized I by SCMFSA6A:26;
then dom I c= dom (Initialized I) by RELAT_1:25;
hence 0 in dom (Initialized I) by A2; :: thesis: verum