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

per cases ( [y,f] 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 Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or [y,f] in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by Z, XBOOLE_0:def 3;

suppose S: [y,f] 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 Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ; :: thesis: f is set

per cases ( [y,f] 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 Element of NAT : verum } or [y,f] in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ) by S, XBOOLE_0:def 3;

suppose S: [y,f] 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 Element of NAT : verum } ; :: thesis: f is set

per cases ( [y,f] 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 [y,f] in { [6,<*i*>,{}] where i is Element of NAT : verum } ) by S, XBOOLE_0:def 3;

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

per cases ( [y,f] in {[0,{},{}]} or [y,f] 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 S, XBOOLE_0:def 3;

suppose [y,f] in {[0,{},{}]} ; :: thesis: f is set

then [y,f] = [0,{},{}] by TARSKI:def 1;
then f = {} by ZFMISC_1:33;
hence f is FinSequence ; :: thesis: verum

end;

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

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

end;

end;

end;

suppose [y,f] in { [6,<*i*>,{}] where i is Element of NAT : verum } ; :: thesis: f is set

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

end;

end;

end;

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

then consider i being Element of NAT , a being Element of SCM-Data-Loc such that
W: [y,f] = [7,<*i*>,<*a*>] ;
f = <*a*> by W, ZFMISC_1:33;
hence f is FinSequence ; :: thesis: verum

end;

end;

end;

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

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

end;

end;