let i1, i2, i3 be Integer; :: thesis: for s being State of SCM st Initialize (((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) c= s holds
s is State-consisting of <%i1,i2,i3%>
set x = ((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3);
let s be State of SCM; :: thesis: ( Initialize (((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) c= s implies s is State-consisting of <%i1,i2,i3%> )
assume A1: Initialize (((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) c= s ; :: thesis: s is State-consisting of <%i1,i2,i3%>
set D = <%i1,i2,i3%>;
let k be Nat; :: according to SCM_1:def 1 :: thesis: ( len <%i1,i2,i3%> <= k or s . (dl. k) = <%i1,i2,i3%> . k )
assume A2: k < len <%i1,i2,i3%> ; :: thesis: s . (dl. k) = <%i1,i2,i3%> . k
len <%i1,i2,i3%> = 2 + 1 by AFINSQ_1:39;
then k <= 2 by A2, NAT_1:13;
then A3: not not k = 0 & ... & not k = 2 ;
A4: ( dl. 0 <> dl. 1 & dl. 0 <> dl. 2 ) by AMI_3:10;
A5: dom (((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) = {(dl. 0),(dl. 1),(dl. 2)} by FUNCT_4:128;
A6: dom (((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) c= dom ((((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) +* (Start-At (0,SCM))) by FUNCT_4:10;
A7: dl. 0 in {(dl. 0),(dl. 1),(dl. 2)} by ENUMSET1:def 1;
dl. 0 <> IC by AMI_5:2;
then not dl. 0 in dom (Start-At (0,SCM)) by TARSKI:def 1;
then A8: ((((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) +* (Start-At (0,SCM))) . (dl. 0) = (((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) . (dl. 0) by FUNCT_4:11
.= i1 by A4, FUNCT_4:134 ;
A9: dl. 1 in {(dl. 0),(dl. 1),(dl. 2)} by ENUMSET1:def 1;
dl. 1 <> IC by AMI_5:2;
then not dl. 1 in dom (Start-At (0,SCM)) by TARSKI:def 1;
then A10: ((((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) +* (Start-At (0,SCM))) . (dl. 1) = (((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) . (dl. 1) by FUNCT_4:11
.= i2 by AMI_3:10, FUNCT_4:135 ;
A11: dl. 2 in {(dl. 0),(dl. 1),(dl. 2)} by ENUMSET1:def 1;
dl. 2 <> IC by AMI_5:2;
then not dl. 2 in dom (Start-At (0,SCM)) by TARSKI:def 1;
then ((((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) +* (Start-At (0,SCM))) . (dl. 2) = (((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) . (dl. 2) by FUNCT_4:11
.= i3 by FUNCT_4:135 ;
hence s . (dl. k) = <%i1,i2,i3%> . k by A1, A3, A5, A6, A7, A8, A9, A10, A11, GRFUNC_1:2; :: thesis: verum