let f be Function of X,X; :: thesis: ( f is reflexive & f is total implies f is bijective )
assume A1: ( f is reflexive & f is total ) ; :: thesis: f is bijective
then A2: f is_reflexive_in field f by RELAT_2:def 9;
A3: field f = (dom f) \/ (rng f) by RELAT_1:def 6;
thus f is one-to-one :: according to FUNCT_2:def 4 :: thesis: f is onto

proof

let x1 be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not x1 in proj1 f or not b₁ in proj1 f or not f . x1 = f . b₁ or x1 = b₁ )
let x2 be set ; :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A4: x1 in dom f and
A5: x2 in dom f and
A6: f . x1 = f . x2 ; :: thesis: x1 = x2
x1 in field f by A3, A4, XBOOLE_0:def 3;
then [x1,x1] in f by A2, RELAT_2:def 1;
then A7: x1 = f . x1 by A4, FUNCT_1:def 2;
x2 in field f by A3, A5, XBOOLE_0:def 3;
then [x2,x2] in f by A2, RELAT_2:def 1;
hence x1 = x2 by A5, A6, A7, FUNCT_1:def 2; :: thesis: verum

end;

thus rng f c= X ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: X c= rng f
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in rng f )
assume x in X ; :: thesis: x in rng f
then x in dom f by A1, PARTFUN1:def 2;
then x in field f by A3, XBOOLE_0:def 3;
then [x,x] in f by A2, RELAT_2:def 1;
hence x in rng f by RELAT_1:def 5; :: thesis: verum