set A = NAT ;
let s be State of SCM+FSA ; :: thesis: (Initialize s) | NAT = s | NAT
A1: Initialize s = (s +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 )) by SCMFSA6C:def 3
.= s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15 ;

now

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

end;

then (dom ((intloc 0 ) .--> 1)) \/ (dom (Start-At (insloc 0 ))) misses NAT by XBOOLE_0:3;
then dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) misses NAT by FUNCT_4:def 1;
hence (Initialize s) | NAT = s | NAT by A1, FUNCT_4:94; :: thesis: verum