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

assume A1: x in SCM-Instr ; :: thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]

assume A1: x in SCM-Instr ; :: thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]

per cases
( x in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } or x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } )
by A1, XBOOLE_0:def 3;

end;

suppose A2:
x in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} }
; :: thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]

end;

per cases
( x in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } or x in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } )
by A2, XBOOLE_0:def 3;

end;

suppose A3:
x in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 }
; :: thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]

end;

per cases
( x in {[SCM-Halt,{},{}]} or x in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } )
by A3, XBOOLE_0:def 3;

end;

suppose
x in {[SCM-Halt,{},{}]}
; :: thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]

then A4:
x = [SCM-Halt,{},{}]
by TARSKI:def 1;

then ( SCM-Halt in NAT & {} in NAT * & {} in proj2 SCM-Instr ) by A1, FINSEQ_1:49, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A4, DOMAIN_1:3; :: thesis: verum

end;then ( SCM-Halt in NAT & {} in NAT * & {} in proj2 SCM-Instr ) by A1, FINSEQ_1:49, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A4, DOMAIN_1:3; :: thesis: verum

suppose
x in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 }
; :: thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]

then consider J being Element of Segm 9, a being Nat such that

A5: ( x = [J,<*a*>,{}] & J = 6 ) ;

( J in NAT & <*a*> in NAT * & {} in proj2 SCM-Instr ) by A1, A5, FUNCT_7:18, XTUPLE_0:def 13, ORDINAL1:def 12;

hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A5, DOMAIN_1:3; :: thesis: verum

end;A5: ( x = [J,<*a*>,{}] & J = 6 ) ;

( J in NAT & <*a*> in NAT * & {} in proj2 SCM-Instr ) by A1, A5, FUNCT_7:18, XTUPLE_0:def 13, ORDINAL1:def 12;

hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A5, DOMAIN_1:3; :: thesis: verum

suppose
x in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} }
; :: thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]

then consider K being Element of Segm 9, a1 being Nat, b1 being Element of SCM-Data-Loc such that

A6: ( x = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;

( K in NAT & <*a1*> in NAT * & <*b1*> in proj2 SCM-Instr ) by A1, A6, FUNCT_7:18, XTUPLE_0:def 13, ORDINAL1:def 12;

hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A6, DOMAIN_1:3; :: thesis: verum

end;A6: ( x = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;

( K in NAT & <*a1*> in NAT * & <*b1*> in proj2 SCM-Instr ) by A1, A6, FUNCT_7:18, XTUPLE_0:def 13, ORDINAL1:def 12;

hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A6, DOMAIN_1:3; :: thesis: verum

suppose
x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} }
; :: thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]

then consider I being Element of Segm 9, b, c being Element of SCM-Data-Loc such that

A7: ( x = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;

( I in NAT & {} in NAT * & <*b,c*> in proj2 SCM-Instr ) by A1, A7, FINSEQ_1:49, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A7, DOMAIN_1:3; :: thesis: verum

end;A7: ( x = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;

( I in NAT & {} in NAT * & <*b,c*> in proj2 SCM-Instr ) by A1, A7, FINSEQ_1:49, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A7, DOMAIN_1:3; :: thesis: verum