let R be good Ring; :: thesis: for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p holds
IC p in dom p
let p be autonomic FinPartState of (SCM R); :: thesis: ( IC (SCM R) in dom p implies IC p in dom p )
assume A1: IC (SCM R) in dom p ; :: thesis: IC p in dom p
assume A2: not IC p in dom p ; :: thesis: contradiction
set il = IC p;
set p1 = p +* ((IC p) .--> (goto (il. (SCM R),0 )));
set p2 = p +* ((IC p) .--> (goto (il. (SCM R),1)));
consider s1 being State of (SCM R) such that
A3: p +* ((IC p) .--> (goto (il. (SCM R),0 ))) c= s1 by CARD_3:97;
consider s2 being State of (SCM R) such that
A4: p +* ((IC p) .--> (goto (il. (SCM R),1))) c= s2 by CARD_3:97;
not p is autonomic

proof

A5: dom ((IC p) .--> (goto (il. (SCM R),1))) = {(IC p)} by FUNCOP_1:19;
A6: dom ((IC p) .--> (goto (il. (SCM R),0 ))) = {(IC p)} by FUNCOP_1:19;
take s1 ; :: according to AMI_1:def 25 :: thesis: ex b₁ being Element of product the Object-Kind of (SCM R) st
( p c= s1 & p c= b₁ & not for b₂ being Element of NAT holds (Computation s1,b₂) | (dom p) = (Computation b₁,b₂) | (dom p) )
take s2 ; :: thesis: ( p c= s1 & p c= s2 & not for b₁ being Element of NAT holds (Computation s1,b₁) | (dom p) = (Computation s2,b₁) | (dom p) )
dom p misses {(IC p)} by A2, ZFMISC_1:56;
then A7: ( p c= p +* ((IC p) .--> (goto (il. (SCM R),0 ))) & p c= p +* ((IC p) .--> (goto (il. (SCM R),1))) ) by A5, A6, FUNCT_4:33;
hence ( p c= s1 & p c= s2 ) by A3, A4, XBOOLE_1:1; :: thesis: not for b₁ being Element of NAT holds (Computation s1,b₁) | (dom p) = (Computation s2,b₁) | (dom p)
take 1 ; :: thesis: not (Computation s1,1) | (dom p) = (Computation s2,1) | (dom p)
A8: IC p in dom ((IC p) .--> (goto (il. (SCM R),1))) by A5, TARSKI:def 1;
A9: IC p in dom ((IC p) .--> (goto (il. (SCM R),0 ))) by A6, TARSKI:def 1;
dom (p +* ((IC p) .--> (goto (il. (SCM R),0 )))) = (dom p) \/ (dom ((IC p) .--> (goto (il. (SCM R),0 )))) by FUNCT_4:def 1;
then IC p in dom (p +* ((IC p) .--> (goto (il. (SCM R),0 )))) by A9, XBOOLE_0:def 3;
then A10: s1 . (IC p) = (p +* ((IC p) .--> (goto (il. (SCM R),0 )))) . (IC p) by A3, GRFUNC_1:8
.= ((IC p) .--> (goto (il. (SCM R),0 ))) . (IC p) by A9, FUNCT_4:14
.= goto (il. (SCM R),0 ) by FUNCOP_1:87 ;
dom (p +* ((IC p) .--> (goto (il. (SCM R),1)))) = (dom p) \/ (dom ((IC p) .--> (goto (il. (SCM R),1)))) by FUNCT_4:def 1;
then IC p in dom (p +* ((IC p) .--> (goto (il. (SCM R),1)))) by A8, XBOOLE_0:def 3;
then A11: s2 . (IC p) = (p +* ((IC p) .--> (goto (il. (SCM R),1)))) . (IC p) by A4, GRFUNC_1:8
.= ((IC p) .--> (goto (il. (SCM R),1))) . (IC p) by A8, FUNCT_4:14
.= goto (il. (SCM R),1) by FUNCOP_1:87 ;
A12: (Following s1) . (IC (SCM R)) = (Exec (goto (il. (SCM R),0 )),s1) . (IC (SCM R)) by A1, A3, A7, A10, AMI_1:97, XBOOLE_1:1
.= il. (SCM R),0 by SCMRING2:17 ;
A13: (Following s2) . (IC (SCM R)) = (Exec (goto (il. (SCM R),1)),s2) . (IC (SCM R)) by A1, A4, A7, A11, AMI_1:97, XBOOLE_1:1
.= il. (SCM R),1 by SCMRING2:17 ;
assume A14: (Computation s1,1) | (dom p) = (Computation s2,1) | (dom p) ; :: thesis: contradiction
A15: (Following s1) | (dom p) = (Following (Computation s1,0 )) | (dom p) by AMI_1:13
.= (Computation s1,(0 + 1)) | (dom p) by AMI_1:14
.= (Following (Computation s2,0 )) | (dom p) by A14, AMI_1:14
.= (Following s2) | (dom p) by AMI_1:13 ;
il. (SCM R),0 = ((Following s1) | (dom p)) . (IC (SCM R)) by A1, A12, FUNCT_1:72
.= il. (SCM R),1 by A1, A13, A15, FUNCT_1:72 ;
hence contradiction by AMISTD_1:25; :: thesis: verum

end;

hence contradiction ; :: thesis: verum