let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SCM+FSA-Instr or x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] )
assume A1: 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, 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} } or x in { [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } ) by A1;

suppose A2: x in (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} } ; :: 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, b, c is Element of SCM-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-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by A2, XBOOLE_0:def 3;

suppose A3: x in 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} } ; :: 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, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) by A3, XBOOLE_0:def 3;

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

then A4: x in [:NAT,(NAT *),(proj2 SCM-Instr):] by SCM_INST:8;
proj2 SCM-Instr c= proj2 SCM+FSA-Instr by Th1, XTUPLE_0:9;
then [:NAT,(NAT *),(proj2 SCM-Instr):] c= [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by MCART_1:73;
hence x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by A4; :: thesis: verum

end;

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

then consider J being Element of Segm 13, b, c being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc such that
A5: ( x = [J,{},<*c,f,b*>] & J in {9,10} ) ;
A6: {} in NAT * by FINSEQ_1:49;
( J in NAT & <*c,f,b*> in proj2 SCM+FSA-Instr ) by A1, A5, XTUPLE_0:def 13;
hence x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by A5, A6, MCART_1:69; :: thesis: verum

end;

end;

end;

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

then consider K being Element of Segm 13, c1 being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc such that
A7: ( x = [K,{},<*c1,f1*>] & K in {11,12} ) ;
A8: {} in NAT * by FINSEQ_1:49;
( K in NAT & <*c1,f1*> in proj2 SCM+FSA-Instr ) by A1, A7, XTUPLE_0:def 13;
hence x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by A7, A8, MCART_1:69; :: thesis: verum

end;

end;

end;

suppose x in { [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } ; :: thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]

then consider b1 being Element of SCM-Data-Loc such that
A9: x = [13,{},<*b1*>] ;
A10: {} in NAT * by FINSEQ_1:49;
for K being Element of Segm 13 holds
( K in NAT & <*b1*> in proj2 SCM+FSA-Instr ) by A1, A9, XTUPLE_0:def 13;
hence x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by A9, A10, MCART_1:69; :: thesis: verum

end;

end;