let I, J, K be Program of ; :: thesis: (I ";" J) ";" K = I ";" (J ";" K)
A1: (card (stop I)) -' 1 = card I by COMPOS_1:71;
A2: card (stop (Directed I)) = card (stop I) by Lm2;
A3: card (stop (Directed (I ";" J))) = card (stop (I ";" J)) by Lm2;
A4: (card (stop (I ";" J))) -' 1 = card (I ";" J) by COMPOS_1:71;
A5: card (stop (Directed J)) = card (stop J) by Lm2;
(card (stop J)) -' 1 = card J by COMPOS_1:71;
then A6: Reloc ((J ";" K),(card I)) = (Reloc ((Directed J),(card I))) +* (Reloc ((Reloc (K,(card J))),(card I))) by COMPOS_1:42, A5
.= (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 Th14, A4, A3
.= (Directed I) +* ((Reloc ((Directed J),(card I))) +* (Reloc (K,(card (I ";" J))))) by FUNCT_4:14, A1, A2
.= I ";" (J ";" K) by A6, Th11, A1, A2 ; :: thesis: verum