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