let I, J be Program of ; :: thesis: Directed I c= I ';' J

A1: now

let x be set ; :: 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 A2: 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 A2, XBOOLE_0:3;
hence (Directed I) . x = (I ';' J) . x by FUNCT_4:11; :: thesis: verum

end;

dom (I ';' J) = (dom (Directed I)) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:def 1;
then dom (Directed I) c= dom (I ';' J) by XBOOLE_1:7;
hence Directed I c= I ';' J by A1, GRFUNC_1:2; :: thesis: verum