let R be good Ring; :: thesis: for p being FinPartState of (SCM R)
for q being FinPartState of SCM st p = q holds
DataPart p = DataPart q
let p be FinPartState of (SCM R); :: thesis: for q being FinPartState of SCM st p = q holds
DataPart p = DataPart q
let q be FinPartState of SCM ; :: thesis: ( p = q implies DataPart p = DataPart q )
assume p = q ; :: thesis: DataPart p = DataPart q
hence DataPart p = q | (the carrier of SCM \ ({(IC (SCM R))} \/ NAT )) by Lm2
.= DataPart q by AMI_3:4, SCMRING2:9 ;
:: thesis: verum