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, Th47, 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