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