let x be set ; :: thesis: for c, b being Element of SCM+FSA-Data-Loc
for f being Element of SCM+FSA-Data*-Loc st x in {9,10} holds
[x,{} ,<*c,f,b*>] in SCM+FSA-Instr
let c, b be Element of SCM+FSA-Data-Loc ; :: thesis: for f being Element of SCM+FSA-Data*-Loc st x in {9,10} holds
[x,{} ,<*c,f,b*>] in SCM+FSA-Instr
let f be Element of SCM+FSA-Data*-Loc ; :: thesis: ( x in {9,10} implies [x,{} ,<*c,f,b*>] in SCM+FSA-Instr )
assume A1: x in {9,10} ; :: thesis: [x,{} ,<*c,f,b*>] in SCM+FSA-Instr
then ( x = 9 or x = 10 ) by TARSKI:def 2;
then reconsider x = x as Element of Segm 13 by NAT_1:45;
[x,{} ,<*c,f,b*>] in { [K,{} ,<*c1,f1,b1*>] where K is Element of Segm 13, c1, b1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {9,10} } by A1;
then [x,{} ,<*c,f,b*>] in SCM-Instr \/ { [K,{} ,<*c1,f1,b1*>] where K is Element of Segm 13, c1, b1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {9,10} } by XBOOLE_0:def 3;
hence [x,{} ,<*c,f,b*>] in SCM+FSA-Instr by XBOOLE_0:def 3; :: thesis: verum