let X, Y be set ; :: thesis: ( X <> {} & Y <> {} implies ( dom [:X,Y:] = X & rng [:X,Y:] = Y ) )
assume that
A1: X <> {} and
A2: 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

consider y being Element of Y;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in dom [:X,Y:] )
assume x in X ; :: thesis: x in dom [:X,Y:]
then [x,y] in [:X,Y:] by 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

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

end;