let I, J be Program of SCMPDS ; :: thesis: for s being State of SCMPDS st Initialized J c= s holds
Initialized I c= s +* I
let s be State of SCMPDS ; :: thesis: ( Initialized J c= s implies Initialized I c= s +* I )
assume Initialized J c= s ; :: thesis: Initialized I c= s +* I
then s +* (Initialized I) = s +* I by Th34;
hence Initialized I c= s +* I by FUNCT_4:26; :: thesis: verum