let f be set ; :: according to FINSEQ_1:def 19 :: thesis: ( not f in proj2 SCMPDS-Instr or f is set )
assume f in proj2 SCMPDS-Instr ; :: thesis: f is set
then consider y being set such that
Z: [y,f] in SCMPDS-Instr by RELAT_1:def 5;
set x = [y,f];

per cases ( [y,f] in (( { [0,{},<*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 14, 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 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or [y,f] in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 14, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by Z, XBOOLE_0:def 3;

suppose S: [y,f] in (( { [0,{},<*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 14, 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 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; :: thesis: f is set

per cases ( [y,f] in ( { [0,{},<*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 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or [y,f] in { [I,{},<*v,c1,c2*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) by S, XBOOLE_0:def 3;

suppose S: [y,f] in ( { [0,{},<*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 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; :: thesis: f is set

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

suppose S: [y,f] in { [0,{},<*l*>] where l is Element of INT : verum } \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; :: thesis: f is set

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

suppose [y,f] in { [0,{},<*l*>] where l is Element of INT : verum } ; :: thesis: f is set

then consider l being Element of INT such that
W: [y,f] = [0,{},<*l*>] ;
f = <*l*> by W, ZFMISC_1:33;
hence f is FinSequence ; :: thesis: verum

end;

suppose [y,f] in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; :: thesis: f is set

then consider sp being Element of SCM-Data-Loc such that
W: [y,f] = [1,{},<*sp*>] ;
f = <*sp*> by W, ZFMISC_1:33;
hence f is FinSequence ; :: thesis: verum

end;

end;

end;

suppose [y,f] in { [I,{},<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; :: thesis: f is set

then consider I being Element of Segm 14, v being Element of SCM-Data-Loc , c being Element of INT such that
W: ( [y,f] = [I,{},<*v,c*>] & I in {2,3} ) ;
f = <*v,c*> by W, ZFMISC_1:33;
hence f is FinSequence ; :: thesis: verum

end;

end;

end;

suppose [y,f] in { [I,{},<*v,c1,c2*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; :: thesis: f is set

then consider I being Element of Segm 14, v being Element of SCM-Data-Loc , c1, c2 being Element of INT such that
W: ( [y,f] = [I,{},<*v,c1,c2*>] & I in {4,5,6,7,8} ) ;
f = <*v,c1,c2*> by W, ZFMISC_1:33;
hence f is FinSequence ; :: thesis: verum

end;

end;

end;

suppose [y,f] in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 14, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ; :: thesis: f is set

then consider I being Element of Segm 14, v1, v2 being Element of SCM-Data-Loc , c1, c2 being Element of INT such that
W: ( [y,f] = [I,{},<*v1,v2,c1,c2*>] & I in {9,10,11,12,13} ) ;
f = <*v1,v2,c1,c2*> by W, ZFMISC_1:33;
hence f is FinSequence ; :: thesis: verum

end;

end;