let I, J be Program of SCM+FSA; :: thesis: ProgramPart (Relocated (J,(card I))) c= I ';' J
I ';' J = (Directed I) +* (ProgramPart (Relocated (J,(card I)))) by SCMFSA6A:def 5;
hence ProgramPart (Relocated (J,(card I))) c= I ';' J by FUNCT_4:26; :: thesis: verum