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

A1: [y,f] in SCM+FSA-Instr by XTUPLE_0:def 13;

set x = [y,f];

assume f in proj2 SCM+FSA-Instr ; :: thesis: f is set

then consider y being object such that

A1: [y,f] in SCM+FSA-Instr by XTUPLE_0:def 13;

set x = [y,f];

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

end;

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

end;

per cases
( [y,f] in SCM-Instr \/ { [J,{},<*c,f1,b*>] where J is Element of Segm 13, b, c is Element of SCM-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-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } )
by A2, XBOOLE_0:def 3;

end;

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

end;

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

end;

suppose
[y,f] in { [J,{},<*c,f1,b*>] where J is Element of Segm 13, b, c is Element of SCM-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, b, c being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc such that

A4: ( [y,f] = [J,{},<*c,f1,b*>] & J in {9,10} ) ;

f = <*c,f1,b*> by A4, XTUPLE_0:1;

hence f is FinSequence ; :: thesis: verum

end;A4: ( [y,f] = [J,{},<*c,f1,b*>] & J in {9,10} ) ;

f = <*c,f1,b*> by A4, XTUPLE_0:1;

hence f is FinSequence ; :: thesis: verum

suppose
[y,f] in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-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-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc such that

A5: ( [y,f] = [K,{},<*c1,f1*>] & K in {11,12} ) ;

f = <*c1,f1*> by A5, XTUPLE_0:1;

hence f is FinSequence ; :: thesis: verum

end;A5: ( [y,f] = [K,{},<*c1,f1*>] & K in {11,12} ) ;

f = <*c1,f1*> by A5, XTUPLE_0:1;

hence f is FinSequence ; :: thesis: verum