let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( I is_closed_onInit s,p iff I is_closed_on Initialized s,p )
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds
( I is_closed_onInit s,p iff I is_closed_on Initialized s,p )
let I be Program of SCM+FSA; :: thesis: ( I is_closed_onInit s,p iff I is_closed_on Initialized s,p )
set s1 = s +* (Initialized I);
set s2 = (Initialized s) +* (Initialize I);
set p1 = p +* I;
A1: ProgramPart I = I by RELAT_1:209;
A2: s +* (Initialized I) = (Initialized s) +* (Initialize I) by SCMFSA8A:13;
( I is_closed_onInit s,p iff for k being Element of NAT holds IC (Comput ((p +* I),(s +* (Initialized I)),k)) in dom I ) by Def4;
hence ( I is_closed_onInit s,p iff I is_closed_on Initialized s,p ) by A2, SCMFSA7B:def 7, A1; :: thesis: verum