let d1 be Element of SCM-Data-Loc ; :: thesis: for G being non empty good 1-sorted holds pi ((product (SCM-OK G)),d1) = the carrier of G
let G be non empty good 1-sorted ; :: thesis: pi ((product (SCM-OK G)),d1) = the carrier of G
dom (SCM-OK G) = SCM-Memory by FUNCT_2:def 1;
hence pi ((product (SCM-OK G)),d1) = (SCM-OK G) . d1 by CARD_3:22
.= the carrier of G by Th3 ;
:: thesis: verum