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