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