let s be State of SCMPDS ; :: thesis: for loc being Element of NAT
for I being Program of SCMPDS st loc in dom I holds
((Initialize s) +* I) . loc = I . loc
let loc be Element of NAT ; :: thesis: for I being Program of SCMPDS st loc in dom I holds
((Initialize s) +* I) . loc = I . loc
let I be Program of SCMPDS ; :: thesis: ( loc in dom I implies ((Initialize s) +* I) . loc = I . loc )
assume loc in dom I ; :: thesis: ((Initialize s) +* I) . loc = I . loc
hence ((Initialize s) +* I) . loc = I . loc by FUNCT_4:14; :: thesis: verum