let X, Y be set ; :: thesis: ( X <> {} & Y <> {} implies ( dom [:X,Y:] = X & rng [:X,Y:] = Y ) )
assume A1: ( X <> {} & Y <> {} ) ; :: thesis: ( dom [:X,Y:] = X & rng [:X,Y:] = Y )
thus dom [:X,Y:] c= X :: according to XBOOLE_0:def 10 :: thesis: ( X c= dom [:X,Y:] & rng [:X,Y:] = Y )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom [:X,Y:] or x in X )
assume x in dom [:X,Y:] ; :: thesis: x in X
then ex y being set st [x,y] in [:X,Y:] by RELAT_1:def 4;
hence x in X by ZFMISC_1:106; :: thesis: verum

end;

thus X c= dom [:X,Y:] :: thesis: rng [:X,Y:] = Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in dom [:X,Y:] )
assume A2: x in X ; :: thesis: x in dom [:X,Y:]
consider y being Element of Y;
[x,y] in [:X,Y:] by A1, A2, ZFMISC_1:106;
hence x in dom [:X,Y:] by RELAT_1:20; :: thesis: verum

end;

thus rng [:X,Y:] c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= rng [:X,Y:]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng [:X,Y:] or y in Y )
assume y in rng [:X,Y:] ; :: thesis: y in Y
then ex x being set st [x,y] in [:X,Y:] by RELAT_1:def 5;
hence y in Y by ZFMISC_1:106; :: thesis: verum

end;

thus Y c= rng [:X,Y:] :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in rng [:X,Y:] )
assume A3: y in Y ; :: thesis: y in rng [:X,Y:]
consider x being Element of X;
[x,y] in [:X,Y:] by A1, A3, ZFMISC_1:106;
hence y in rng [:X,Y:] by RELAT_1:20; :: thesis: verum

end;