let s be State of SCMPDS ; :: thesis: ( IC s = 0 implies Initialize s = s )
assume A1: IC s = 0 ; :: thesis: Initialize s = s
A2: IC SCMPDS in dom s by COMPOS_1:9;
thus Initialize s = s +* ((IC SCMPDS ) .--> 0 )
.= s by A1, A2, FUNCT_7:111 ; :: thesis: verum