let s be State of SCM+FSA ; :: thesis: (Initialize 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 AMI_1:137;
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;
Initialize s = (s +* ((intloc 0 ) .--> 1)) +* (Start-At 0 ,SCM+FSA ) by SCMFSA6C:def 3
.= s +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:15 ;
hence (Initialize s) | NAT = s | NAT by A3, FUNCT_4:94; :: thesis: verum