let d1 be Element of SCM-Data-Loc ; :: thesis: pi ((product SCMPDS-OK),d1) = INT
dom SCMPDS-OK = SCM-Memory by FUNCT_2:def 1;
hence pi ((product SCMPDS-OK),d1) = SCMPDS-OK . d1 by CARD_3:12
.= INT by Th19 ;
:: thesis: verum