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