let n be Element of NAT ; :: thesis: for I being Program of SCMPDS
for x being set st x in dom I holds
I . x = (I +* (Start-At n,SCMPDS )) . x
let I be Program of SCMPDS ; :: thesis: for x being set st x in dom I holds
I . x = (I +* (Start-At n,SCMPDS )) . x
let x be set ; :: thesis: ( x in dom I implies I . x = (I +* (Start-At n,SCMPDS )) . x )
assume x in dom I ; :: thesis: I . x = (I +* (Start-At n,SCMPDS )) . x
then reconsider l = x as Element of NAT ;
( dom (Start-At n,SCMPDS ) = {(IC SCMPDS )} & l <> IC SCMPDS ) by COMPOS_1:3, FUNCOP_1:19;
then not x in dom (Start-At n,SCMPDS ) by TARSKI:def 1;
hence I . x = (I +* (Start-At n,SCMPDS )) . x by FUNCT_4:12; :: thesis: verum