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,(),(X *):]
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SCMPDS-Instr or x in [:NAT,(),(X *):] )
assume A2: x in SCMPDS-Instr ; :: thesis: x in [:NAT,(),(X *):]
A3: {} in NAT * by FINSEQ_1:49;
per cases ( x in ((( \/ { [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 ;
suppose x in ((( \/ { [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,(),(X *):]
per cases then ( x in (( \/ { [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;
suppose A4: x in (( \/ { [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,(),(X *):]
per cases ( x in ( \/ { [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 ;
suppose A5: x in ( \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; :: thesis: x in [:NAT,(),(X *):]
per cases ( x in \/ { [14,{},<*l*>] where l is Element of INT : verum } or x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) by ;
suppose x in \/ { [14,{},<*l*>] where l is Element of INT : verum } ; :: thesis: x in [:NAT,(),(X *):]
per cases then ( x in or x in { [14,{},<*l*>] where l is Element of INT : verum } ) by XBOOLE_0:def 3;
suppose x in { [14,{},<*l*>] where l is Element of INT : verum } ; :: thesis: x in [:NAT,(),(X *):]
then consider l being Element of INT such that
A7: x = [14,{},<*l*>] ;
<*l*> in proj2 SCMPDS-Instr by ;
hence x in [:NAT,(),(X *):] by ; :: thesis: verum
end;
end;
end;
suppose x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; :: thesis: x in [:NAT,(),(X *):]
then consider sp being Element of SCM-Data-Loc such that
A8: x = [1,{},<*sp*>] ;
<*sp*> in proj2 SCMPDS-Instr by ;
hence x in [:NAT,(),(X *):] by ; :: thesis: verum
end;
end;
end;
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,(),(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 ;
hence x in [:NAT,(),(X *):] by ; :: thesis: verum
end;
end;
end;
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,(),(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 ;
hence x in [:NAT,(),(X *):] by ; :: thesis: verum
end;
end;
end;
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,(),(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 ;
hence x in [:NAT,(),(X *):] by ; :: thesis: verum
end;
end;