let f be object ; FINSEQ_1:def 18 ( not f in proj2 (SCM-Instr S) or f is set )
assume
f in proj2 (SCM-Instr S)
; f is set
then consider y being object such that
A1:
[y,f] in SCM-Instr S
by XTUPLE_0:def 13;
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 Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is 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 A1, XBOOLE_0:def 3;
suppose A2:
[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 Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum }
;
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 Nat : verum } or [y,f] in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } )
by A2, XBOOLE_0:def 3;
suppose A3:
[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 Nat : verum }
;
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 Nat : verum } )
by A3, XBOOLE_0:def 3;
suppose A4:
[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} }
;
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 A4, XBOOLE_0:def 3;
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} }
;
f is set then consider I being
Element of
Segm 8,
a,
b being
Element of
SCM-Data-Loc such that A5:
(
[y,f] = [I,{},<*a,b*>] &
I in {1,2,3,4} )
;
f = <*a,b*>
by A5, XTUPLE_0:1;
hence
f is
FinSequence
;
verum end; end; end; end; end; end; end; end;