let s be State of SCM+FSA; :: thesis: (Initialized s) | NAT = s | NAT
set A = NAT ;

now

let x be set ; :: thesis: ( x in NAT implies not x in (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) )
A1: dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:19;
assume x in NAT ; :: thesis: not x in (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA)))
then reconsider l = x as Element of NAT ;
A2: not l in dom (Start-At (0,SCM+FSA)) by COMPOS_1:29;
l <> intloc 0 by SCMFSA_2:84;
then not x in dom ((intloc 0) .--> 1) by A1, TARSKI:def 1;
hence not x in (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

then (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) misses NAT by XBOOLE_0:3;
then A3: dom (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) misses NAT by FUNCT_4:def 1;
Initialized s = (s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))
.= s +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15 ;
hence (Initialized s) | NAT = s | NAT by A3, FUNCT_4:76; :: thesis: verum