let X be set ; :: thesis: for R being total Relation of X holds field R = X
let R be total Relation of X; :: thesis: field R = X
thus field R = X \/ (rng R) by PARTFUN1:def 2
.= X by XBOOLE_1:12 ; :: thesis: verum