reconsider b = b as PartFunc of X,NAT by Lm7;
b * x c= [:NAT,NAT:] ;
hence x * b is PartFunc of NAT,NAT ; :: thesis: verum