let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA
for l being Element of NAT holds DataPart s = DataPart (s +* (I +* (Start-At l,SCM+FSA )))
let I be Program of SCM+FSA ; :: thesis: for l being Element of NAT holds DataPart s = DataPart (s +* (I +* (Start-At l,SCM+FSA )))
let l be Element of NAT ; :: thesis: DataPart s = DataPart (s +* (I +* (Start-At l,SCM+FSA )))

now

let x be set ; :: thesis: ( x in dom (I +* (Start-At l,SCM+FSA )) implies not b₁ in Int-Locations \/ FinSeq-Locations )
assume x in dom (I +* (Start-At l,SCM+FSA )) ; :: thesis: not b₁ in Int-Locations \/ FinSeq-Locations
then x in (dom I) \/ (dom (Start-At l,SCM+FSA )) by FUNCT_4:def 1;
then ( x in dom I or x in dom (Start-At l,SCM+FSA ) ) by XBOOLE_0:def 3;
then A1: ( x in dom I or x in {(IC SCM+FSA )} ) by FUNCOP_1:19;

per cases ( x in dom I or x = IC SCM+FSA ) by A1, TARSKI:def 1;

suppose A2: x in dom I ; :: thesis: not b₁ in Int-Locations \/ FinSeq-Locations

( dom I c= NAT & Int-Locations \/ FinSeq-Locations misses NAT ) by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
hence not x in Int-Locations \/ FinSeq-Locations by A2, XBOOLE_0:3; :: thesis: verum

end;

suppose x = IC SCM+FSA ; :: thesis: not b₁ in Int-Locations \/ FinSeq-Locations

hence not x in Int-Locations \/ FinSeq-Locations by SCMFSA6A:37; :: thesis: verum

end;

end;

end;

then dom (I +* (Start-At l,SCM+FSA )) misses Int-Locations \/ FinSeq-Locations by XBOOLE_0:3;
hence DataPart s = DataPart (s +* (I +* (Start-At l,SCM+FSA ))) by FUNCT_4:76, SCMFSA_2:127; :: thesis: verum