let S be non empty 1-sorted ; :: thesis: for s being SCM-State of S holds dom s = SCM-Memory
let s be SCM-State of S; :: thesis: dom s = SCM-Memory
dom s = dom ((SCM-VAL S) * SCM-OK) by CARD_3:9;
hence dom s = SCM-Memory by Lm1; :: thesis: verum