let S be non empty 1-sorted ; :: thesis: SCM-Instr S c= [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
set X = proj2 (SCM-Instr S);
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in SCM-Instr S or u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] )
assume A1: u in SCM-Instr S ; :: thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
A2: {} in NAT * by FINSEQ_1:49;

per cases ( u in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } or u in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by A1, XBOOLE_0:def 3;

suppose A3: u in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ; :: thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]

per cases ( u in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } or u in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ) by A3, XBOOLE_0:def 3;

suppose A4: u in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ; :: thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]

per cases ( u in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or u in { [6,<*i*>,{}] where i is Nat : verum } ) by A4, XBOOLE_0:def 3;

suppose A5: u in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ; :: thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]

per cases ( u in {[0,{},{}]} or u in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) by A5, XBOOLE_0:def 3;

suppose u in {[0,{},{}]} ; :: thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]

then A6: u = [0,{},{}] by TARSKI:def 1;
then ( 0 in NAT & {} in proj2 (SCM-Instr S) ) by A1, XTUPLE_0:def 13;
hence u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A6, A2, MCART_1:69; :: thesis: verum

end;

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

then consider I being Element of Segm 8, a, b being Element of SCM-Data-Loc such that
A7: ( u = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
( I in NAT & <*a,b*> in proj2 (SCM-Instr S) ) by A7, A1, XTUPLE_0:def 13;
hence u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A7, A2, MCART_1:69; :: thesis: verum

end;

end;

end;

suppose u in { [6,<*i*>,{}] where i is Nat : verum } ; :: thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]

then consider i being Nat such that
A8: u = [6,<*i*>,{}] ;
i in NAT by ORDINAL1:def 12;
then A9: <*i*> in NAT * by FUNCT_7:18;
( 6 in NAT & {} in proj2 (SCM-Instr S) ) by A8, A1, XTUPLE_0:def 13;
hence u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A8, A9, MCART_1:69; :: thesis: verum

end;

end;

end;

suppose u in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ; :: thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]

then consider i being Nat, a being Element of SCM-Data-Loc such that
A10: u = [7,<*i*>,<*a*>] ;
i in NAT by ORDINAL1:def 12;
then A11: <*i*> in NAT * by FUNCT_7:18;
( 7 in NAT & <*a*> in proj2 (SCM-Instr S) ) by A10, A1, XTUPLE_0:def 13;
hence u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A10, A11, MCART_1:69; :: thesis: verum

end;

end;

end;

suppose u in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ; :: thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]

then consider a being Element of SCM-Data-Loc , r being Element of S such that
A12: u = [5,{},<*a,r*>] ;
( 5 in NAT & <*a,r*> in proj2 (SCM-Instr S) ) by A12, A1, XTUPLE_0:def 13;
hence u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A12, A2, MCART_1:69; :: thesis: verum

end;

end;