let I, J be Program of ; :: thesis: Directed I c= I ";" J
A1: (card (stop I)) -' 1 = card I by COMPOS_1:71;
A2: card (stop (Directed I)) = card (stop I) by Lm2;
A3: now :: thesis: for x being object st x in dom (Directed I) holds
(Directed I) . x = (I ";" J) . x
let x be object ; :: thesis: ( x in dom (Directed I) implies (Directed I) . x = (I ";" J) . x )
assume x in dom (Directed I) ; :: thesis: (Directed I) . x = (I ";" J) . x
then A4: x in dom I by FUNCT_4:99;
dom I misses dom (Reloc (J,(card I))) by COMPOS_1:48;
then not x in dom (Reloc (J,(card I))) by A4, XBOOLE_0:3;
hence (Directed I) . x = (I ";" J) . x by FUNCT_4:11, A1, A2; :: thesis: verum
end;
dom (I ";" J) = (dom (Directed I)) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:def 1, A1, A2;
then dom (Directed I) c= dom (I ";" J) by XBOOLE_1:7;
hence Directed I c= I ";" J by A3, GRFUNC_1:2; :: thesis: verum