let I, J be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st Initialized J c= s holds
Initialized I c= s +* I
let s be State of SCM+FSA ; :: 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 Th51;
hence Initialized I c= s +* I by FUNCT_4:26; :: thesis: verum