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