to_matrix returns a matrix containing ones and zeros. f.to_matrix i j is 1 if f i = some j and 0 otherwise

Restatement of single_mul_single, which will simplify expressions in simp normal form, when associativity may otherwise need to be carefully applied.