let i be Instruction of SCMPDS ; :: thesis: for s being State of SCMPDS
for I being Program of SCMPDS holds CurInstr (ProgramPart (s +* (Initialize (stop (i ';' I))))),((Initialize s) +* (stop (i ';' I))) = i
let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds CurInstr (ProgramPart (s +* (Initialize (stop (i ';' I))))),((Initialize s) +* (stop (i ';' I))) = i
let I be Program of SCMPDS ; :: thesis: CurInstr (ProgramPart (s +* (Initialize (stop (i ';' I))))),((Initialize s) +* (stop (i ';' I))) = i
set iI = i ';' I;
set s3 = s +* (Initialize (stop (i ';' I)));
I1: s +* (Initialize (stop (i ';' I))) = (Initialize s) +* (stop (i ';' I)) by SCMPDS_4:5;
A1: 0 in dom (Load i) by SCMPDS_5:2;
card (i ';' I) = (card I) + 1 by Th15;
then A2: 0 in dom (i ';' I) by AFINSQ_1:70;
Y: (ProgramPart ((Initialize s) +* (stop (i ';' I)))) /. (IC ((Initialize s) +* (stop (i ';' I)))) = ((Initialize s) +* (stop (i ';' I))) . (IC ((Initialize s) +* (stop (i ';' I)))) by COMPOS_1:38;
i ';' I c= Initialize (stop (i ';' I)) by Th17;
then dom (i ';' I) c= dom (Initialize (stop (i ';' I))) by GRFUNC_1:8;
then (s +* (Initialize (stop (i ';' I)))) . 0 = (Initialize (stop (i ';' I))) . 0 by A2, FUNCT_4:14
.= (i ';' I) . 0 by A2, Th20
.= ((Load i) ';' I) . 0
.= (Load i) . 0 by A1, SCMPDS_4:37
.= i by SCMPDS_5:4 ;
hence CurInstr (ProgramPart (s +* (Initialize (stop (i ';' I))))),((Initialize s) +* (stop (i ';' I))) = i by Y, I1, FUNCT_4:26, SCMPDS_5:18; :: thesis: verum