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