let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA
for l being Element of NAT
for x being set st x in dom I holds
I . x = (s +* (I +* (Start-At (l,SCM+FSA)))) . x
let I be Program of SCM+FSA; :: thesis: for l being Element of NAT
for x being set st x in dom I holds
I . x = (s +* (I +* (Start-At (l,SCM+FSA)))) . x
let l be Element of NAT ; :: thesis: for x being set st x in dom I holds
I . x = (s +* (I +* (Start-At (l,SCM+FSA)))) . x
let x be set ; :: thesis: ( x in dom I implies I . x = (s +* (I +* (Start-At (l,SCM+FSA)))) . x )
assume A1: x in dom I ; :: thesis: I . x = (s +* (I +* (Start-At (l,SCM+FSA)))) . x
reconsider y = x as Element of NAT by A1;
A2: not y in dom (Start-At (l,SCM+FSA)) by COMPOS_1:29;
x in dom (I +* (Start-At (l,SCM+FSA))) by A1, FUNCT_4:13;
hence (s +* (I +* (Start-At (l,SCM+FSA)))) . x = (I +* (Start-At (l,SCM+FSA))) . x by FUNCT_4:14
.= I . x by A2, FUNCT_4:12 ;
:: thesis: verum