let s be State of SCM+FSA; :: thesis: ( IC (Initialized s) = 0 & (Initialized s) . (intloc 0) = 1 & ( for a being read-write Int-Location holds (Initialized s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialized s) . f = s . f ) & ( for l being Element of NAT holds (Initialized s) . l = s . l ) )
A1: ((intloc 0) .--> 1) . (intloc 0) = 1 by FUNCOP_1:87;
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
then A2: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
A3: Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:15;
(Start-At (0,SCM+FSA)) . (IC ) = 0 by FUNCOP_1:87;
hence IC (Initialized s) = 0 by A2, FUNCT_4:14, A3; :: thesis: ( (Initialized s) . (intloc 0) = 1 & ( for a being read-write Int-Location holds (Initialized s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialized s) . f = s . f ) & ( for l being Element of NAT holds (Initialized s) . l = s . l ) )
A4: dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:19;
then A5: intloc 0 in dom ((intloc 0) .--> 1) by TARSKI:def 1;
not intloc 0 in dom (Start-At (0,SCM+FSA)) by SCMFSA6B:9;
hence (Initialized s) . (intloc 0) = (s +* ((intloc 0) .--> 1)) . (intloc 0) by FUNCT_4:12, A3
.= 1 by A5, A1, FUNCT_4:14 ;
:: thesis: ( ( for a being read-write Int-Location holds (Initialized s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialized s) . f = s . f ) & ( for l being Element of NAT holds (Initialized s) . l = s . l ) )

hereby :: thesis: ( ( for f being FinSeq-Location holds (Initialized s) . f = s . f ) & ( for l being Element of NAT holds (Initialized s) . l = s . l ) )

let a be read-write Int-Location ; :: thesis: (Initialized s) . a = s . a
A6: not a in dom ((intloc 0) .--> 1) by A4, TARSKI:def 1;
not a in dom (Start-At (0,SCM+FSA)) by SCMFSA6B:9;
hence (Initialized s) . a = (s +* ((intloc 0) .--> 1)) . a by FUNCT_4:12, A3
.= s . a by A6, FUNCT_4:12 ;
:: thesis: verum

end;

hereby :: thesis: for l being Element of NAT holds (Initialized s) . l = s . l

let f be FinSeq-Location ; :: thesis: (Initialized s) . f = s . f
intloc 0 <> f by SCMFSA_2:83;
then A7: not f in dom ((intloc 0) .--> 1) by A4, TARSKI:def 1;
not f in dom (Start-At (0,SCM+FSA)) by SCMFSA6B:10;
hence (Initialized s) . f = (s +* ((intloc 0) .--> 1)) . f by FUNCT_4:12, A3
.= s . f by A7, FUNCT_4:12 ;
:: thesis: verum

end;

let l be Element of NAT ; :: thesis: (Initialized s) . l = s . l
intloc 0 <> l by SCMFSA_2:84;
then A8: not l in dom ((intloc 0) .--> 1) by A4, TARSKI:def 1;
not l in dom (Start-At (0,SCM+FSA)) by COMPOS_1:29;
hence (Initialized s) . l = (s +* ((intloc 0) .--> 1)) . l by FUNCT_4:12, A3
.= s . l by A8, FUNCT_4:12 ;
:: thesis: verum