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

A1: now

let x be set ; :: thesis: ( x in dom I implies I . x = (I ';' J) . x )
assume A2: x in dom I ; :: thesis: I . x = (I ';' J) . x
dom I misses dom (Shift J,(card I)) by AFINSQ_1:76;
then not x in dom (Shift J,(card I)) by A2, XBOOLE_0:3;
hence I . x = (I ';' J) . x by FUNCT_4:12; :: thesis: verum

end;

dom I c= dom (I ';' J) by Th39;
hence I c= I ';' J by A1, GRFUNC_1:8; :: thesis: verum