let R be non trivial good Ring; :: thesis: for a being Data-Location of R
for il, i1 being Instruction-Location of SCM R holds NIC (a =0_goto i1),il = {i1,(Next il)}
let a be Data-Location of R; :: thesis: for il, i1 being Instruction-Location of SCM R holds NIC (a =0_goto i1),il = {i1,(Next il)}
let il, i1 be Instruction-Location of SCM R; :: thesis: NIC (a =0_goto i1),il = {i1,(Next il)}
consider t being State of ;
reconsider I = a =0_goto i1 as Element of ObjectKind il by AMI_1:def 14;
reconsider a' = a as Element of SCM-Data-Loc by SCMRING2:1;
A1: ObjectKind a = (SCM-OK R) . a' by SCMRING2:def 1
.= the carrier of R by SCMRING1:5 ;
il in NAT by AMI_1:def 4;
then A2: a <> il by Th2;
il in NAT by AMI_1:def 4;
then reconsider il1 = il as Element of ObjectKind (IC (SCM R)) by AMI_1:def 11;
thus NIC (a =0_goto i1),il c= {i1,(Next il)} by Th61; :: according to XBOOLE_0:def 10 :: thesis: {i1,(Next il)} c= NIC (a =0_goto i1),il
set u = t +* ((IC (SCM R)),il --> il1,I);
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {i1,(Next il)} or x in NIC (a =0_goto i1),il )
A3: IC (SCM R) <> a by Th3;
assume A4: x in {i1,(Next il)} ; :: thesis: x in NIC (a =0_goto i1),il

per cases ( x = i1 or x = Next il ) by A4, TARSKI:def 2;

suppose A5: x = i1 ; :: thesis: x in NIC (a =0_goto i1),il

reconsider 0R = 0. R as Element of ObjectKind a by A1;
set v = (t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> 0R);
A6: dom ((IC (SCM R)),il --> il1,I) = {(IC (SCM R)),il} by FUNCT_4:65;
then A7: IC (SCM R) in dom ((IC (SCM R)),il --> il1,I) by TARSKI:def 2;
A8: il in dom ((IC (SCM R)),il --> il1,I) by A6, TARSKI:def 2;
A9: dom (a .--> 0R) = {a} by FUNCOP_1:19;
then not IC (SCM R) in dom (a .--> 0R) by A3, TARSKI:def 1;
then A10: IC ((t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> 0R)) = (t +* ((IC (SCM R)),il --> il1,I)) . (IC (SCM R)) by FUNCT_4:12
.= ((IC (SCM R)),il --> il1,I) . (IC (SCM R)) by A7, FUNCT_4:14
.= il by AMI_1:48, FUNCT_4:66 ;
not il in dom (a .--> 0R) by A2, A9, TARSKI:def 1;
then A11: ((t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> 0R)) . il = (t +* ((IC (SCM R)),il --> il1,I)) . il by FUNCT_4:12
.= ((IC (SCM R)),il --> il1,I) . il by A8, FUNCT_4:14
.= I by FUNCT_4:66 ;
a in dom (a .--> 0R) by A9, TARSKI:def 1;
then ((t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> 0R)) . a = (a .--> 0R) . a by FUNCT_4:14
.= 0. R by FUNCOP_1:87 ;
then IC (Following ((t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> 0R))) = i1 by A10, A11, SCMRING2:18;
hence x in NIC (a =0_goto i1),il by A5, A10, A11; :: thesis: verum

end;

suppose A12: x = Next il ; :: thesis: x in NIC (a =0_goto i1),il

consider e being Element of such that
A13: e <> 0. R by STRUCT_0:def 19;
reconsider E = e as Element of ObjectKind a by A1;
set v = (t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> E);
A14: dom ((IC (SCM R)),il --> il1,I) = {(IC (SCM R)),il} by FUNCT_4:65;
then A15: IC (SCM R) in dom ((IC (SCM R)),il --> il1,I) by TARSKI:def 2;
A16: il in dom ((IC (SCM R)),il --> il1,I) by A14, TARSKI:def 2;
A17: dom (a .--> E) = {a} by FUNCOP_1:19;
then not IC (SCM R) in dom (a .--> E) by A3, TARSKI:def 1;
then A18: IC ((t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> E)) = (t +* ((IC (SCM R)),il --> il1,I)) . (IC (SCM R)) by FUNCT_4:12
.= ((IC (SCM R)),il --> il1,I) . (IC (SCM R)) by A15, FUNCT_4:14
.= il by AMI_1:48, FUNCT_4:66 ;
not il in dom (a .--> E) by A2, A17, TARSKI:def 1;
then A19: ((t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> E)) . il = (t +* ((IC (SCM R)),il --> il1,I)) . il by FUNCT_4:12
.= ((IC (SCM R)),il --> il1,I) . il by A16, FUNCT_4:14
.= I by FUNCT_4:66 ;
a in dom (a .--> E) by A17, TARSKI:def 1;
then ((t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> E)) . a = (a .--> E) . a by FUNCT_4:14
.= E by FUNCOP_1:87 ;
then IC (Following ((t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> E))) = Next il by A13, A18, A19, SCMRING2:18;
hence x in NIC (a =0_goto i1),il by A12, A18, A19; :: thesis: verum

end;

end;