let a be Element of SCM-Data-Loc ; :: thesis: pi ((product (SCM-VAL * SCM-OK)),a) = INT
thus pi ((product (SCM-VAL * SCM-OK)),a) = (SCM-VAL * SCM-OK) . a by Lm5, CARD_3:12
.= INT by Th2 ; :: thesis: verum