consider X being non empty set such that

A1: proj2 SCMPDS-Instr c= X * by FINSEQ_1:85;

take X ; :: according to COMPOS_0:def 1 :: thesis: SCMPDS-Instr c= [:NAT,(NAT *),(X *):]

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

assume A2: x in SCMPDS-Instr ; :: thesis: x in [:NAT,(NAT *),(X *):]

A3: {} in NAT * by FINSEQ_1:49;

A1: proj2 SCMPDS-Instr c= X * by FINSEQ_1:85;

take X ; :: according to COMPOS_0:def 1 :: thesis: SCMPDS-Instr c= [:NAT,(NAT *),(X *):]

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

assume A2: x in SCMPDS-Instr ; :: thesis: x in [:NAT,(NAT *),(X *):]

A3: {} in NAT * by FINSEQ_1:49;

per cases
( x in ((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } )
by A2, XBOOLE_0:def 3;

end;

suppose
x in ((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} }
; :: thesis: x in [:NAT,(NAT *),(X *):]

end;

per cases then
( x in (({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } )
by XBOOLE_0:def 3;

end;

suppose A4:
x in (({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} }
; :: thesis: x in [:NAT,(NAT *),(X *):]

end;

per cases
( x in ({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } or x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } )
by A4, XBOOLE_0:def 3;

end;

suppose A5:
x in ({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum }
; :: thesis: x in [:NAT,(NAT *),(X *):]

end;

per cases
( x in {[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } or x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } )
by A5, XBOOLE_0:def 3;

end;

suppose
x in {[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum }
; :: thesis: x in [:NAT,(NAT *),(X *):]

end;

per cases then
( x in {[0,{},{}]} or x in { [14,{},<*l*>] where l is Element of INT : verum } )
by XBOOLE_0:def 3;

end;

suppose
x in {[0,{},{}]}
; :: thesis: x in [:NAT,(NAT *),(X *):]

then A6:
x = [0,{},{}]
by TARSKI:def 1;

{} in X * by FINSEQ_1:49;

hence x in [:NAT,(NAT *),(X *):] by A6, A3, MCART_1:69; :: thesis: verum

end;{} in X * by FINSEQ_1:49;

hence x in [:NAT,(NAT *),(X *):] by A6, A3, MCART_1:69; :: thesis: verum

suppose
x in { [14,{},<*l*>] where l is Element of INT : verum }
; :: thesis: x in [:NAT,(NAT *),(X *):]

then consider l being Element of INT such that

A7: x = [14,{},<*l*>] ;

<*l*> in proj2 SCMPDS-Instr by A2, A7, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(X *):] by A1, A7, A3, MCART_1:69; :: thesis: verum

end;A7: x = [14,{},<*l*>] ;

<*l*> in proj2 SCMPDS-Instr by A2, A7, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(X *):] by A1, A7, A3, MCART_1:69; :: thesis: verum

suppose
x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum }
; :: thesis: x in [:NAT,(NAT *),(X *):]

then consider sp being Element of SCM-Data-Loc such that

A8: x = [1,{},<*sp*>] ;

<*sp*> in proj2 SCMPDS-Instr by A2, A8, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(X *):] by A1, A8, A3, MCART_1:69; :: thesis: verum

end;A8: x = [1,{},<*sp*>] ;

<*sp*> in proj2 SCMPDS-Instr by A2, A8, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(X *):] by A1, A8, A3, MCART_1:69; :: thesis: verum

suppose
x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} }
; :: thesis: x in [:NAT,(NAT *),(X *):]

then consider I being Element of Segm 15, v being Element of SCM-Data-Loc , c being Element of INT such that

A9: ( x = [I,{},<*v,c*>] & I in {2,3} ) ;

<*v,c*> in proj2 SCMPDS-Instr by A2, A9, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(X *):] by A1, A9, A3, MCART_1:69; :: thesis: verum

end;A9: ( x = [I,{},<*v,c*>] & I in {2,3} ) ;

<*v,c*> in proj2 SCMPDS-Instr by A2, A9, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(X *):] by A1, A9, A3, MCART_1:69; :: thesis: verum

suppose
x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} }
; :: thesis: x in [:NAT,(NAT *),(X *):]

then consider I being Element of Segm 15, v being Element of SCM-Data-Loc , c1, c2 being Element of INT such that

A10: ( x = [I,{},<*v,c1,c2*>] & I in {4,5,6,7,8} ) ;

<*v,c1,c2*> in proj2 SCMPDS-Instr by A2, A10, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(X *):] by A1, A10, A3, MCART_1:69; :: thesis: verum

end;A10: ( x = [I,{},<*v,c1,c2*>] & I in {4,5,6,7,8} ) ;

<*v,c1,c2*> in proj2 SCMPDS-Instr by A2, A10, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(X *):] by A1, A10, A3, MCART_1:69; :: thesis: verum

suppose
x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} }
; :: thesis: x in [:NAT,(NAT *),(X *):]

then consider I being Element of Segm 15, v1, v2 being Element of SCM-Data-Loc , c1, c2 being Element of INT such that

A11: ( x = [I,{},<*v1,v2,c1,c2*>] & I in {9,10,11,12,13} ) ;

<*v1,v2,c1,c2*> in proj2 SCMPDS-Instr by A2, A11, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(X *):] by A1, A11, A3, MCART_1:69; :: thesis: verum

end;A11: ( x = [I,{},<*v1,v2,c1,c2*>] & I in {9,10,11,12,13} ) ;

<*v1,v2,c1,c2*> in proj2 SCMPDS-Instr by A2, A11, XTUPLE_0:def 13;

hence x in [:NAT,(NAT *),(X *):] by A1, A11, A3, MCART_1:69; :: thesis: verum