let I, J, K be Program of SCM+FSA; :: thesis: (I ';' J) ';' K = I ';' (J ';' K)
A1: ProgramPart (Relocated ((J ';' K),(card I))) = (ProgramPart (Relocated ((Directed J),(card I)))) +* (ProgramPart (Relocated ((ProgramPart (Relocated (K,(card J)))),(card I)))) by Th21
.= (ProgramPart (Relocated ((Directed J),(card I)))) +* (ProgramPart (Relocated (K,((card J) + (card I))))) by Th22 ;
thus (I ';' J) ';' K = (I ';' (Directed J)) +* (ProgramPart (Relocated (K,(card (I ';' J))))) by Th66
.= (Directed I) +* ((ProgramPart (Relocated ((Directed J),(card I)))) +* (ProgramPart (Relocated (K,(card (I ';' J)))))) by FUNCT_4:15
.= I ';' (J ';' K) by A1, Th61 ; :: thesis: verum