let I, J be Program of SCM+FSA; :: thesis: for x being set st x in dom I holds
(I ";" J) . x = (Directed I) . x
let x be set ; :: thesis: ( x in dom I implies (I ";" J) . x = (Directed I) . x )
assume x in dom I ; :: thesis: (I ";" J) . x = (Directed I) . x
then A1: x in dom (Directed I) by FUNCT_4:99;
Directed I c= I ";" J by SCMFSA6A:16;
hence (I ";" J) . x = (Directed I) . x by A1, GRFUNC_1:2; :: thesis: verum