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;
( dom (Start-At (0,SCM+FSA)) = {(IC SCM+FSA)} & x <> IC SCM+FSA ) 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
.= I . x by A2, FUNCT_4:12 ;
:: thesis: verum