let I, J, K be Program of SCM+FSA ; :: thesis: (I ';' J) ';' K = I ';' (J ';' K)
XX: 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 Th52
.= (Directed I) +* ((ProgramPart (Relocated (Directed J),(card I))) +* (ProgramPart (Relocated K,(card (I ';' J))))) by FUNCT_4:15
.= I ';' (J ';' K) by XX, Th61 ; :: thesis: verum