let I be Instruction of SCM+FSA; :: thesis: ( InsCode I = 0 implies I = [0,{},{}] )
assume A1: InsCode I = 0 ; :: thesis: I = [0,{},{}]

A2: now :: thesis: not I in { [R,{},<*DA,DC*>] where R is Element of Segm 9, DA, DC is Element of SCM-Data-Loc : R in {1,2,3,4,5} }

assume I in { [R,{},<*DA,DC*>] where R is Element of Segm 9, DA, DC is Element of SCM-Data-Loc : R in {1,2,3,4,5} } ; :: thesis: contradiction
then ex R being Element of Segm 9 ex DA, DC being Element of SCM-Data-Loc st
( I = [R,{},<*DA,DC*>] & R in {1,2,3,4,5} ) ;
hence contradiction by A1; :: thesis: verum

end;

A3: now :: thesis: not I in { [O,<*LA*>,{}] where O is Element of Segm 9, LA is Nat : O = 6 }

assume I in { [O,<*LA*>,{}] where O is Element of Segm 9, LA is Nat : O = 6 } ; :: thesis: contradiction
then ex O being Element of Segm 9 ex LA being Nat st
( I = [O,<*LA*>,{}] & O = 6 ) ;
hence contradiction by A1; :: thesis: verum

end;

A4: now :: thesis: not I in { [P,<*LB*>,<*DB*>] where P is Element of Segm 9, LB is Nat, DB is Element of SCM-Data-Loc : P in {7,8} }

assume I in { [P,<*LB*>,<*DB*>] where P is Element of Segm 9, LB is Nat, DB is Element of SCM-Data-Loc : P in {7,8} } ; :: thesis: contradiction
then ex P being Element of Segm 9 ex LB being Nat ex DB being Element of SCM-Data-Loc st
( I = [P,<*LB*>,<*DB*>] & P in {7,8} ) ;
hence contradiction by A1; :: thesis: verum

end;

A5: now :: thesis: not I in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} }

assume I in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ; :: thesis: contradiction
then ex K being Element of Segm 13 ex dC being Element of SCM+FSA-Data-Loc ex fB being Element of SCM+FSA-Data*-Loc st
( I = [K,{},<*dC,fB*>] & K in {11,12} ) ;
hence contradiction by A1; :: thesis: verum

end;

A6: I in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } by A5, XBOOLE_0:def 3;

now :: thesis: not I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} }

assume I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ; :: thesis: contradiction
then ex L being Element of Segm 13 ex dA, dB being Element of SCM+FSA-Data-Loc ex fA being Element of SCM+FSA-Data*-Loc st
( I = [L,{},<*dB,fA,dA*>] & L in {9,10} ) ;
hence contradiction by A1; :: thesis: verum

end;

then I in SCM-Instr by A6, XBOOLE_0:def 3;
then I in ({[SCM-Halt,{},{}]} \/ { [O,<*LA*>,{}] where O is Element of Segm 9, LA is Nat : O = 6 } ) \/ { [P,<*LB*>,<*DB*>] where P is Element of Segm 9, LB is Nat, DB is Element of SCM-Data-Loc : P in {7,8} } by A2, XBOOLE_0:def 3;
then I in {[SCM-Halt,{},{}]} \/ { [O,<*LA*>,{}] where O is Element of Segm 9, LA is Nat : O = 6 } by A4, XBOOLE_0:def 3;
then I in {[SCM-Halt,{},{}]} by A3, XBOOLE_0:def 3;
hence I = [0,{},{}] by TARSKI:def 1; :: thesis: verum