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;