dom C = I by PARTFUN1:def 2;
then C . i in rng C by FUNCT_1:3;
hence for b₁ being RelStr st b₁ = C . i holds
b₁ is transitive by Def4; :: thesis: verum