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