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
( Initialized I is_closed_on 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
( Initialized I is_closed_on s,P iff I is_closed_on Initialized s,P )
let I be Program of SCM+FSA; :: thesis: ( Initialized I is_closed_on s,P iff I is_closed_on Initialized s,P )
A1: ProgramPart I = I by RELAT_1:209;
A2: ProgramPart (Initialized I) = I by SCMFSA6A:33;

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

assume A3: Initialized I is_closed_on s,P ; :: thesis: I is_closed_on Initialized s,P

now

let k be Element of NAT ; :: thesis: IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),k)) in dom I
A4: s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I) by Th16;
IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),k)) in dom (Initialized I) by A3, SCMFSA7B:def 7, A2;
then IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),k)) in dom (Initialized I) by A4;
hence IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),k)) in dom I by Th20; :: thesis: verum

end;

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

end;

assume A5: I is_closed_on Initialized s,P ; :: thesis: Initialized I is_closed_on s,P

now

let k be Element of NAT ; :: thesis: IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),k)) in dom (Initialized I)
A6: s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I) by Th16;
IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),k)) in dom I by A5, SCMFSA7B:def 7, A1;
then IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),k)) in dom (Initialized I) by Th20;
hence IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),k)) in dom (Initialized I) by A6; :: thesis: verum

end;

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