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

per cases ( [y,f] in SCM-Instr \/ { [J,{},<*c,f1,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : J in {9,10} } or [y,f] in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by Z, XBOOLE_0:def 3;

suppose S: [y,f] in SCM-Instr \/ { [J,{},<*c,f1,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : J in {9,10} } ; :: thesis: f is set

per cases ( [y,f] in SCM-Instr or [y,f] in { [J,{},<*c,f1,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) by S, XBOOLE_0:def 3;

suppose [y,f] in SCM-Instr ; :: thesis: f is set

then f in proj2 SCM-Instr by RELAT_1:def 5;
hence f is FinSequence ; :: thesis: verum

end;

suppose [y,f] in { [J,{},<*c,f1,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : J in {9,10} } ; :: thesis: f is set

then consider J being Element of Segm 13, c, b being Element of SCM+FSA-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc such that
W: ( [y,f] = [J,{},<*c,f1,b*>] & J in {9,10} ) ;
f = <*c,f1,b*> by W, ZFMISC_1:33;
hence f is FinSequence ; :: thesis: verum

end;

end;

end;

suppose [y,f] in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ; :: thesis: f is set

then consider K being Element of Segm 13, c1 being Element of SCM+FSA-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc such that
W: ( [y,f] = [K,{},<*c1,f1*>] & K in {11,12} ) ;
f = <*c1,f1*> by W, ZFMISC_1:33;
hence f is FinSequence ; :: thesis: verum

end;

end;