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