let f be object ; :: according to FINSEQ_1:def 18 :: 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 object such that

A1: [y,f] in SCMPDS-Instr by XTUPLE_0:def 13;

set x = [y,f];

assume f in proj2 SCMPDS-Instr ; :: thesis: f is set

then consider y being object such that

A1: [y,f] in SCMPDS-Instr by XTUPLE_0:def 13;

set x = [y,f];

per cases
( [y,f] 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 [y,f] 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 A1, XBOOLE_0:def 3;

end;

suppose A2:
[y,f] 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: f is set

end;

per cases
( [y,f] 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 [y,f] 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 A2, XBOOLE_0:def 3;

end;

suppose
[y,f] 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: f is set

then
[y,f] 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} }
by XBOOLE_1:4;

then ( [y,f] in {[0,{},{}]} \/ ( { [14,{},<*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 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) by XBOOLE_0:def 3;

end;then ( [y,f] in {[0,{},{}]} \/ ( { [14,{},<*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 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) by XBOOLE_0:def 3;

per cases then
( [y,f] in {[0,{},{}]} or [y,f] in { [14,{},<*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 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } )
by XBOOLE_0:def 3;

end;

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

end;

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

end;

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

then
ex l being Element of INT st [y,f] = [14,{},<*l*>]
;

hence f is FinSequence by XTUPLE_0:1; :: thesis: verum

end;hence f is FinSequence by XTUPLE_0:1; :: thesis: verum

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

then
ex sp being Element of SCM-Data-Loc st [y,f] = [1,{},<*sp*>]
;

hence f is FinSequence by XTUPLE_0:1; :: thesis: verum

end;hence f is FinSequence by XTUPLE_0:1; :: thesis: verum

suppose
[y,f] 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: f is set

then
ex I being Element of Segm 15 ex v being Element of SCM-Data-Loc ex c being Element of INT st

( [y,f] = [I,{},<*v,c*>] & I in {2,3} ) ;

hence f is FinSequence by XTUPLE_0:1; :: thesis: verum

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

hence f is FinSequence by XTUPLE_0:1; :: thesis: verum

suppose
[y,f] 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: f is set

then
ex I being Element of Segm 15 ex v being Element of SCM-Data-Loc ex c1, c2 being Element of INT st

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

hence f is FinSequence by XTUPLE_0:1; :: thesis: verum

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

hence f is FinSequence by XTUPLE_0:1; :: thesis: verum

suppose
[y,f] 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: f is set

then
ex I being Element of Segm 15 ex v1, v2 being Element of SCM-Data-Loc ex c1, c2 being Element of INT st

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

hence f is FinSequence by XTUPLE_0:1; :: thesis: verum

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

hence f is FinSequence by XTUPLE_0:1; :: thesis: verum