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

per cases ( [y,f] in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or [y,f] in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ) by Z, XBOOLE_0:def 3;

suppose S: [y,f] in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } ; :: thesis: f is set

per cases ( [y,f] in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } or [y,f] in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } ) by S, XBOOLE_0:def 3;

suppose S: [y,f] in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ; :: thesis: f is set

per cases ( [y,f] in {[SCM-Halt,{},{}]} or [y,f] in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ) by S, XBOOLE_0:def 3;

suppose [y,f] in {[SCM-Halt,{},{}]} ; :: thesis: f is set

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

end;

suppose [y,f] in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ; :: thesis: f is set

then consider J being Element of Segm 9, a being Element of NAT such that
W: ( [y,f] = [J,<*a*>,{}] & J = 6 ) ;
f = {} by W, ZFMISC_1:33;
hence f is FinSequence ; :: thesis: verum

end;

end;

end;

suppose [y,f] in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } ; :: thesis: f is set

then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of SCM-Data-Loc such that
W: ( [y,f] = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
f = <*b1*> by W, ZFMISC_1:33;
hence f is FinSequence ; :: thesis: verum

end;

end;

end;

suppose [y,f] in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ; :: thesis: f is set

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

end;

end;