dom C = I by PARTFUN1:def 2;
then C . i in rng C by FUNCT_1:3;
hence for b₁ being TolStr st b₁ = C . i holds
b₁ is pcs-tol-reflexive by Def16; :: thesis: verum