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

(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