let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds
( I is_closed_onInit s iff I is_closed_on Initialized s )
let I be Program of SCM+FSA ; :: thesis: ( I is_closed_onInit s iff I is_closed_on Initialized s )
set s1 = s +* (Initialized I);
set s2 = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ));
A1: s +* (Initialized I) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
( I is_closed_onInit s iff for k being Element of NAT holds IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) in dom I ) by Def4;
hence ( I is_closed_onInit s iff I is_closed_on Initialized s ) by A1, SCMFSA7B:def 7; :: thesis: verum