let s be State of SCMPDS ; :: thesis: ( IC s = 0 implies Initialized s = s )
assume A1: IC s = 0 ; :: thesis: Initialized s = s
A2: IC SCMPDS in dom s by AMI_1:94;
thus Initialized s = s +* ((IC SCMPDS ) .--> 0 ) by SCMPDS_5:def 4
.= s by A1, A2, FUNCT_7:111 ; :: thesis: verum