let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS
for n being Element of NAT st IC (Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n) = 0 holds
(Initialize (Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n)) +* I = Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n
let I be Program of SCMPDS ; :: thesis: for n being Element of NAT st IC (Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n) = 0 holds
(Initialize (Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n)) +* I = Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n
let n be Element of NAT ; :: thesis: ( IC (Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n) = 0 implies (Initialize (Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n)) +* I = Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n )
I1: (Initialize s) +* I = s +* (Initialize I) by SCMPDS_4:5;
set sn = Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n;
A1: Initialize I c= (Initialize s) +* I by I1, FUNCT_4:26;
I c= I +* (Start-At 0 ,SCMPDS ) by SCMPDS_6:6;
then I c= (Initialize s) +* I by A1, XBOOLE_1:1;
then A2: I c= Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n by AMI_1:81;
assume IC (Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n) = 0 ; :: thesis: (Initialize (Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n)) +* I = Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n
then (Initialize (Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n)) +* I = (Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n) +* I by Th4;
hence (Initialize (Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n)) +* I = Comput (ProgramPart ((Initialize s) +* I)),((Initialize s) +* I),n by A2, FUNCT_4:79; :: thesis: verum