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 )
A2: s +* (Initialize ((intloc 0) .--> 1)) = s +* (Initialize (Initialize ((intloc 0) .--> 1))) by FUNCT_4:99
.= Initialize (Initialized s) by FUNCT_4:15 ;

hereby :: thesis: ( I is_closed_on Initialized s,p implies I is_closed_onInit s,p )

assume Z: I is_closed_onInit s,p ; :: thesis: I is_closed_on Initialized s,p
thus I is_closed_on Initialized s,p :: thesis: verum

proof

let k be Element of NAT ; :: according to SCMFSA7B:def 7 :: thesis: IC (Comput ((p +* I),(Initialize (Initialized s)),k)) in K250(I)
IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) in dom I by Z, Def4;
hence IC (Comput ((p +* I),(Initialize (Initialized s)),k)) in dom I by A2; :: thesis: verum

end;

end;

assume Z: I is_closed_on Initialized s,p ; :: thesis: I is_closed_onInit s,p
let k be Element of NAT ; :: according to SCM_HALT:def 4 :: thesis: IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) in dom I
IC (Comput ((p +* I),(Initialize (Initialized s)),k)) in dom I by Z, SCMFSA7B:def 7;
hence IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) in dom I by A2; :: thesis: verum