A1: SCM-Instr \/ { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } c= SCM+FSA-Instr by XBOOLE_1:7;
SCM-Instr c= SCM-Instr \/ { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } by XBOOLE_1:7;
hence SCM-Instr c= SCM+FSA-Instr by A1, XBOOLE_1:1; :: thesis: verum