let s be State of SCM+FSA ; :: thesis: for I being paraclosed Program of SCM+FSA holds 0 in dom I
let I be paraclosed Program of SCM+FSA ; :: thesis: 0 in dom I
I is_closed_on s by SCMFSA7B:24;
hence 0 in dom I by Th39; :: thesis: verum