let ins be Instruction of SCM ; :: thesis: ( InsCode ins = 5 implies ex da, db being Data-Location st ins = Divide da,db )
assume A1: InsCode ins = 5 ; :: thesis: ex da, db being Data-Location st ins = Divide da,db

A2: now

assume ins in { [J,<*a*>,{} ] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; :: thesis: contradiction
then ex J being Element of Segm 9 ex a being Element of NAT st
( ins = [J,<*a*>,{} ] & J = 6 ) ;
hence contradiction by A1, RECDEF_2:def 1; :: thesis: verum

end;

A3: now

assume ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } ; :: thesis: contradiction
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of SCM-Data-Loc such that
A4: ins = [K,<*a1*>,<*b1*>] and
A5: K in {7,8} ;
InsCode ins = K by A4, RECDEF_2:def 1;
hence contradiction by A1, A5, TARSKI:def 2; :: thesis: verum

end;

not ins in {[SCM-Halt ,{} ,{} ]} by A1, Th37, AMI_3:71, TARSKI:def 1;
then not ins in {[SCM-Halt ,{} ,{} ]} \/ { [J,<*a*>,{} ] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A2, XBOOLE_0:def 3;
then not ins in ({[SCM-Halt ,{} ,{} ]} \/ { [J,<*a*>,{} ] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } by A3, XBOOLE_0:def 3;
then ins 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 XBOOLE_0:def 3;
then consider I being Element of Segm 9, b, c being Element of SCM-Data-Loc such that
A6: ins = [I,{} ,<*b,c*>] and
I in {1,2,3,4,5} ;
reconsider da = b @ , db = c @ as Data-Location ;
take da ; :: thesis: ex db being Data-Location st ins = Divide da,db
take db ; :: thesis: ins = Divide da,db
thus ins = Divide da,db by A1, A6, RECDEF_2:def 1; :: thesis: verum