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

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

set x = [y,f];

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

then consider y being object such that

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

set x = [y,f];

per cases
( [y,f] in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is 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 A1, XBOOLE_0:def 3;

end;

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

end;

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

end;

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

end;

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

end;

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

then
ex K being Element of Segm 9 ex a1 being Nat ex b1 being Element of SCM-Data-Loc st

( [y,f] = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;

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

end;( [y,f] = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;

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

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
ex I being Element of Segm 9 ex b, c being Element of SCM-Data-Loc st

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

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

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

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