let I be Program of SCM+FSA ; :: thesis: for x being set st x in dom I holds
I . x = (Initialized I) . x
let x be set ; :: thesis: ( x in dom I implies I . x = (Initialized I) . x )
assume A1: x in dom I ; :: thesis: I . x = (Initialized I) . x
A2: dom ((intloc 0 ) .--> 1) = {(intloc 0 )} by FUNCOP_1:19;
x <> intloc 0 by A1, Th47;
then A3: not x in dom ((intloc 0 ) .--> 1) by A2, TARSKI:def 1;
A4: dom (Start-At (insloc 0 )) = {(IC SCM+FSA )} by FUNCOP_1:19;
x <> IC SCM+FSA by A1, Th47;
then not x in dom (Start-At (insloc 0 )) by A4, TARSKI:def 1;
hence (Initialized I) . x = (I +* ((intloc 0 ) .--> 1)) . x by FUNCT_4:12
.= I . x by A3, FUNCT_4:12 ;
:: thesis: verum