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
A2: 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, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f . x1 = f . x2 ; :: thesis: x1 = x2
x1 in field f by A2, A3, XBOOLE_0:def 3;
then [x1,x1] in f by A1, RELAT_2:def 1, RELAT_2:def 9;
then A6: x1 = f . x1 by A3, FUNCT_1:def 2;
x2 in field f by A2, A4, XBOOLE_0:def 3;
then [x2,x2] in f by A1, RELAT_2:def 1, RELAT_2:def 9;
hence x1 = x2 by A4, A5, A6, 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 object ; :: 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 PARTFUN1:def 2;
then x in field f by A2, XBOOLE_0:def 3;
then [x,x] in f by A1, RELAT_2:def 1, RELAT_2:def 9;
hence x in rng f by XTUPLE_0:def 13; :: thesis: verum