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