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
then ( dom ((intloc 0) .--> 1) = {(intloc 0)} & x <> intloc 0 ) by Th47, FUNCOP_1:19;
then A2: not x in dom ((intloc 0) .--> 1) by TARSKI:def 1;
A3: Initialized I = Initialize (I +* ((intloc 0) .--> 1)) by FUNCT_4:15;
( dom (Start-At (0,SCM+FSA)) = {(IC )} & x <> IC ) by A1, COMPOS_1:139, FUNCOP_1:19;
then not x in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
hence (Initialized I) . x = (I +* ((intloc 0) .--> 1)) . x by FUNCT_4:12, A3
.= I . x by A2, FUNCT_4:12 ;
:: thesis: verum