set D = Int-Locations \/ FinSeq-Locations ;
let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st s . (intloc 0 ) = 1 holds
( I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s )
let I be Program of SCM+FSA ; :: thesis: ( s . (intloc 0 ) = 1 implies ( I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s ) )
assume s . (intloc 0 ) = 1 ; :: thesis: ( I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s )
then DataPart s = DataPart (Initialize s) by Th27;
hence ( I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s ) by Th52; :: thesis: verum