let G be non empty 1-sorted ; :: thesis: for a being Element of SCM-Data-Loc holds pi ((product ((SCM-VAL G) * SCM-OK)),a) = the carrier of G
let a be Element of SCM-Data-Loc ; :: thesis: pi ((product ((SCM-VAL G) * SCM-OK)),a) = the carrier of G
a in SCM-Memory ;
then a in dom ((SCM-VAL G) * SCM-OK) by Lm1;
hence pi ((product ((SCM-VAL G) * SCM-OK)),a) = ((SCM-VAL G) * SCM-OK) . a by CARD_3:12
.= the carrier of G by Th2 ;
:: thesis: verum