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