let T be InsType of SCM+FSA; :: thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 or T = 9 or T = 10 or T = 11 or T = 12 )
consider y being set such that
B1: [T,y] in proj1 the Instructions of SCM+FSA by RELAT_1:def 4;
consider x being set such that
A1: [[T,y],x] in the Instructions of SCM+FSA by B1, RELAT_1:def 4;
reconsider I = [T,y,x] as Instruction of SCM+FSA by A1;
A2: ( [T,y,x] in SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } or [T,y,x] 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 A1, XBOOLE_0:def 3;

per cases ( [T,y,x] in SCM-Instr or [T,y,x] in { [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } or [T,y,x] 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 A2, XBOOLE_0:def 3;

suppose [T,y,x] in SCM-Instr ; :: thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 or T = 9 or T = 10 or T = 11 or T = 12 )

then reconsider I = [T,y,x] as Instruction of SCM ;
T = InsCode I by RECDEF_2:def 1;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 or T = 9 or T = 10 or T = 11 or T = 12 ) by AMI_6:7; :: thesis: verum

end;

suppose [T,y,x] in { [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ; :: thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 or T = 9 or T = 10 or T = 11 or T = 12 )

then ex J being Element of Segm 13 ex c, b being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( [T,y,x] = [J,{},<*c,f,b*>] & J in {9,10} ) ;
then T in {9,10} by MCART_1:28;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 or T = 9 or T = 10 or T = 11 or T = 12 ) by TARSKI:def 2; :: thesis: verum

end;

suppose [T,y,x] 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: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 or T = 9 or T = 10 or T = 11 or T = 12 )

then ex K being Element of Segm 13 ex c1 being Element of SCM+FSA-Data-Loc ex f1 being Element of SCM+FSA-Data*-Loc st
( [T,y,x] = [K,{},<*c1,f1*>] & K in {11,12} ) ;
then T in {11,12} by MCART_1:28;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 or T = 9 or T = 10 or T = 11 or T = 12 ) by TARSKI:def 2; :: thesis: verum

end;

end;