let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SCM+FSA-Instr or x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] )
assume Z: x in SCM+FSA-Instr ; :: thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]

per cases ( x in 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} } or x in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by Z, XBOOLE_0:def 3;

suppose S: x in 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} } ; :: thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]

per cases ( x in SCM-Instr or x in { [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 S, XBOOLE_0:def 3;

suppose x in SCM-Instr ; :: thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]

then X: x in [:NAT,(NAT *),(proj2 SCM-Instr):] by AMI_2:34;
proj2 SCM-Instr c= proj2 SCM+FSA-Instr by Th2, FUNCT_5:5;
then [:NAT,(NAT *),(proj2 SCM-Instr):] c= [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by MCART_1:77;
hence x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by X; :: thesis: verum

end;

suppose x in { [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} } ; :: thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]

then consider J being Element of Segm 13, c, b being Element of SCM+FSA-Data-Loc , f being Element of SCM+FSA-Data*-Loc such that
W: ( x = [J,{},<*c,f,b*>] & J in {9,10} ) ;
X: {} in NAT * by FINSEQ_1:66;
( J in NAT & <*c,f,b*> in proj2 SCM+FSA-Instr ) by Z, W, RELAT_1:def 5;
hence x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by W, MCART_1:73, X; :: thesis: verum

end;

end;

end;

suppose x in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ; :: thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]

then consider K being Element of Segm 13, c1 being Element of SCM+FSA-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc such that
W: ( x = [K,{},<*c1,f1*>] & K in {11,12} ) ;
X: {} in NAT * by FINSEQ_1:66;
( K in NAT & <*c1,f1*> in proj2 SCM+FSA-Instr ) by Z, W, RELAT_1:def 5;
hence x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by W, MCART_1:73, X; :: thesis: verum

end;

end;