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