dom C = I by PARTFUN1:def 2;
hence C . i is TolStr by Def14; :: thesis: verum