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):]

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;

end;

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):]

end;

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;

end;

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):]

end;

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;

end;

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;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

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;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

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;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

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;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