let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds
( Initialized I is_closed_on s iff I is_closed_on Initialized s )
let I be Program of SCM+FSA ; :: thesis: ( Initialized I is_closed_on s iff I is_closed_on Initialized s )

hereby :: thesis: ( I is_closed_on Initialized s implies Initialized I is_closed_on s )

assume A1: Initialized I is_closed_on s ; :: thesis: I is_closed_on Initialized s

now

let k be Element of NAT ; :: thesis: IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom I
X: s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by Th16;
IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),k) in dom (Initialized I) by A1, SCMFSA7B:def 7;
then IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom (Initialized I) by X;
hence IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom I by Th20; :: thesis: verum

end;

hence I is_closed_on Initialized s by SCMFSA7B:def 7; :: thesis: verum

end;

assume A2: I is_closed_on Initialized s ; :: thesis: Initialized I is_closed_on s

now

let k be Element of NAT ; :: thesis: IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),k) in dom (Initialized I)
X: s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by Th16;
IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom I by A2, SCMFSA7B:def 7;
then IC (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom (Initialized I) by Th20;
hence IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),k) in dom (Initialized I) by X; :: thesis: verum

end;

hence Initialized I is_closed_on s by SCMFSA7B:def 7; :: thesis: verum