let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( not x in dom sumSCMFunction or ex b₁ being set st
( x = b₁ & (Start-At (0,SCM)) +* b₁ is Autonomy of IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))) & sumSCMFunction . b₁ c= Result ((IterativeAlgorithm (AddTo ((dl. 2),(dl. 1)))),((Start-At (0,SCM)) +* b₁)) ) )
assume A1: x in dom sumSCMFunction ; :: thesis: ex b₁ being set st
( x = b₁ & (Start-At (0,SCM)) +* b₁ is Autonomy of IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))) & sumSCMFunction . b₁ c= Result ((IterativeAlgorithm (AddTo ((dl. 2),(dl. 1)))),((Start-At (0,SCM)) +* b₁)) )
then consider n being Nat such that
A2: x = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) by Th37;
reconsider d = x as FinPartState of SCM by A2;
consider s being State of SCM such that
A3: Initialize d c= s by PBOOLE:141;
consider P being Instruction-Sequence of SCM such that
A4: IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))) c= P by PBOOLE:145;
A5: P is IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))) -extending Instruction-Sequence of SCM by A4, PROOFS_1:def 12;
take d ; :: thesis: ( x = d & (Start-At (0,SCM)) +* d is Autonomy of IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))) & sumSCMFunction . d c= Result ((IterativeAlgorithm (AddTo ((dl. 2),(dl. 1)))),((Start-At (0,SCM)) +* d)) )
thus x = d ; :: thesis: ( (Start-At (0,SCM)) +* d is Autonomy of IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))) & sumSCMFunction . d c= Result ((IterativeAlgorithm (AddTo ((dl. 2),(dl. 1)))),((Start-At (0,SCM)) +* d)) )
A6: Initialize d = (Start-At (0,SCM)) +* d by A2, MEMSTR_0:82;
hence (Start-At (0,SCM)) +* d is Autonomy of IterativeAlgorithm (AddTo ((dl. 2),(dl. 1))) by A1, Th39; :: thesis: sumSCMFunction . d c= Result ((IterativeAlgorithm (AddTo ((dl. 2),(dl. 1)))),((Start-At (0,SCM)) +* d))
then A7: Result ((IterativeAlgorithm (AddTo ((dl. 2),(dl. 1)))),((Start-At (0,SCM)) +* d)) = (Result (P,s)) | (dom ((Start-At (0,SCM)) +* d)) by A3, A4, A6, EXTPRO_1:def 13;
A8: sumSCMFunction . d = (dl. 2) .--> H₁(n) by A2, Th38;
A9: s is 0 -started State-consisting of <%1,n,0%> by A2, A3, Th15, MEMSTR_0:17;
set f = (Result (P,s)) | (dom ((Start-At (0,SCM)) +* d));
A10: dom d c= dom ((Start-At (0,SCM)) +* d) by FUNCT_4:10;
dl. 2 in the carrier of SCM ;
then A11: dl. 2 in dom (Result (P,s)) by PARTFUN1:def 2;
dl. 2 in {(dl. 0),(dl. 1),(dl. 2)} by ENUMSET1:def 1;
then dl. 2 in dom d by A2, FUNCT_4:128;
then A12: dl. 2 in dom ((Result (P,s)) | (dom ((Start-At (0,SCM)) +* d))) by A10, A11, RELAT_1:57;
then ((Result (P,s)) | (dom ((Start-At (0,SCM)) +* d))) . (dl. 2) = (Result (P,s)) . (dl. 2) by FUNCT_1:47
.= H₁(n) by A5, A9, Th31 ;
hence sumSCMFunction . d c= Result ((IterativeAlgorithm (AddTo ((dl. 2),(dl. 1)))),((Start-At (0,SCM)) +* d)) by A7, A8, A12, FUNCT_4:85; :: thesis: verum