let s be 0 -started State of SCMPDS; :: thesis: for I being Program of SCMPDS
for n being Element of NAT st IC (Comput ((ProgramPart (s +* I)),(s +* I),n)) = 0 holds
(Initialize (Comput ((ProgramPart (s +* I)),(s +* I),n))) +* I = Comput ((ProgramPart (s +* I)),(s +* I),n)
let I be Program of SCMPDS; :: thesis: for n being Element of NAT st IC (Comput ((ProgramPart (s +* I)),(s +* I),n)) = 0 holds
(Initialize (Comput ((ProgramPart (s +* I)),(s +* I),n))) +* I = Comput ((ProgramPart (s +* I)),(s +* I),n)
let n be Element of NAT ; :: thesis: ( IC (Comput ((ProgramPart (s +* I)),(s +* I),n)) = 0 implies (Initialize (Comput ((ProgramPart (s +* I)),(s +* I),n))) +* I = Comput ((ProgramPart (s +* I)),(s +* I),n) )
set sn = Comput ((ProgramPart (s +* I)),(s +* I),n);
I c= s +* I by FUNCT_4:26;
then A2: I c= Comput ((ProgramPart (s +* I)),(s +* I),n) by AMI_1:81;
assume IC (Comput ((ProgramPart (s +* I)),(s +* I),n)) = 0 ; :: thesis: (Initialize (Comput ((ProgramPart (s +* I)),(s +* I),n))) +* I = Comput ((ProgramPart (s +* I)),(s +* I),n)
then (Initialize (Comput ((ProgramPart (s +* I)),(s +* I),n))) +* I = (Comput ((ProgramPart (s +* I)),(s +* I),n)) +* I by COMPOS_1:84;
hence (Initialize (Comput ((ProgramPart (s +* I)),(s +* I),n))) +* I = Comput ((ProgramPart (s +* I)),(s +* I),n) by A2, FUNCT_4:79; :: thesis: verum