let R be good Ring; :: thesis: for p being FinPartState of
for q being FinPartState of st p = q holds
DataPart p = DataPart q
let p be FinPartState of ; :: thesis: for q being FinPartState of st p = q holds
DataPart p = DataPart q
let q be FinPartState of ; :: 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