let s be State of SCM+FSA; :: 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 ) )
A1: Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:14;
hereby :: thesis: for f being FinSeq-Location holds (Initialized s) . f = s . f
let a be read-write Int-Location; :: thesis: (Initialized s) . a = s . a
A3: not a in dom ((intloc 0) .--> 1) by TARSKI:def 1;
not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
hence (Initialized s) . a = (s +* ((intloc 0) .--> 1)) . a by A1, FUNCT_4:11
.= s . a by A3, FUNCT_4:11 ;
:: thesis: verum
end;
hereby :: thesis: verum
let f be FinSeq-Location ; :: thesis: (Initialized s) . f = s . f
intloc 0 <> f by SCMFSA_2:58;
then A4: not f in dom ((intloc 0) .--> 1) by TARSKI:def 1;
not f in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:103;
hence (Initialized s) . f = (s +* ((intloc 0) .--> 1)) . f by A1, FUNCT_4:11
.= s . f by A4, FUNCT_4:11 ;
:: thesis: verum
end;