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:105;
Directed I c= I ';' J by SCMFSA6A:55;
hence (I ';' J) . x = (Directed I) . x by A1, GRFUNC_1:8; :: thesis: verum