let A, X, Y be set ; :: thesis: for R being Relation of X,Y st id A c= R holds

( A c= dom R & A c= rng R )

let R be Relation of X,Y; :: thesis: ( id A c= R implies ( A c= dom R & A c= rng R ) )

assume A1: id A c= R ; :: thesis: ( A c= dom R & A c= rng R )

thus A c= dom R :: thesis: A c= rng R

( A c= dom R & A c= rng R )

let R be Relation of X,Y; :: thesis: ( id A c= R implies ( A c= dom R & A c= rng R ) )

assume A1: id A c= R ; :: thesis: ( A c= dom R & A c= rng R )

thus A c= dom R :: thesis: A c= rng R

proof

thus
A c= rng R
:: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in dom R )

assume x in A ; :: thesis: x in dom R

then [x,x] in id A by RELAT_1:def 10;

hence x in dom R by A1, XTUPLE_0:def 12; :: thesis: verum

end;assume x in A ; :: thesis: x in dom R

then [x,x] in id A by RELAT_1:def 10;

hence x in dom R by A1, XTUPLE_0:def 12; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in rng R )

assume x in A ; :: thesis: x in rng R

then [x,x] in id A by RELAT_1:def 10;

hence x in rng R by A1, XTUPLE_0:def 13; :: thesis: verum

end;assume x in A ; :: thesis: x in rng R

then [x,x] in id A by RELAT_1:def 10;

hence x in rng R by A1, XTUPLE_0:def 13; :: thesis: verum