A1: SCM-Instr c= SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } by XBOOLE_1:7;
SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } c= (SCM-Instr \/ { [J1,{},<*c2,f2,b2*>] where J1 is Element of Segm 13, b2, c2 is Element of SCM-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : J1 in {9,10} } ) \/ { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } by XBOOLE_1:7;
then A2: SCM-Instr c= (SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } by A1;
thus SCM-Instr c= SCM+FSA-Instr by A2; :: thesis: verum