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 ) by SCMFSA6A:def 4
.= 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