A1: SCM+FSA-OK . NAT = 0 by Lm4;
thus (SCM*-VAL * SCM+FSA-OK) . NAT = SCM*-VAL . (SCM+FSA-OK . NAT) by Lm3, FUNCT_1:13
.= NAT by A1 ; :: thesis: verum