let I, J, K be Program of ; :: thesis: (I ';' J) ';' K = I ';' (J ';' K)
A1: Reloc ((J ';' K),(card I)) = (Reloc ((Directed J),(card I))) +* (Reloc ((Reloc (K,(card J))),(card I))) by COMPOS_1:42
.= (Reloc ((Directed J),(card I))) +* (Reloc (K,((card J) + (card I)))) by COMPOS_1:43 ;
thus (I ';' J) ';' K = (I ';' (Directed J)) +* (Reloc (K,(card (I ';' J)))) by Th66
.= (Directed I) +* ((Reloc ((Directed J),(card I))) +* (Reloc (K,(card (I ';' J))))) by FUNCT_4:14
.= I ';' (J ';' K) by A1, Th61 ; :: thesis: verum