let s be State of ; :: thesis: for I, J being Program of holds
( I is_closed_on Initialize s iff I is_closed_on s +* (Initialized J) )
let I, J be Program of ; :: thesis: ( I is_closed_on Initialize s iff I is_closed_on s +* (Initialized J) )
DataPart (Initialize s) = DataPart (s +* (Initialized J)) by Th5;
hence ( I is_closed_on Initialize s iff I is_closed_on s +* (Initialized J) ) by Th6; :: thesis: verum