let X, Y be set ; :: thesis: ( X <> {} & Y <> {} implies ( dom [:X,Y:] = X & rng [:X,Y:] = Y ) )
assume X <> {} ; :: thesis: ( not Y <> {} or ( dom [:X,Y:] = X & rng [:X,Y:] = Y ) )
then consider a being set such that
A1: a in X by XBOOLE_0:def 1;
assume Y <> {} ; :: thesis: ( dom [:X,Y:] = X & rng [:X,Y:] = Y )
then consider b being set such that
A2: b in Y by XBOOLE_0:def 1;

A3: now

let x be set ; :: thesis: ( x in X implies ex y being set st [x,y] in [:X,Y:] )
assume x in X ; :: thesis: ex y being set st [x,y] in [:X,Y:]
then [x,b] in [:X,Y:] by A2, ZFMISC_1:87;
hence ex y being set st [x,y] in [:X,Y:] ; :: thesis: verum

end;

for x being set st ex y being set st [x,y] in [:X,Y:] holds
x in X by ZFMISC_1:87;
hence dom [:X,Y:] = X by A3, Def4; :: thesis: rng [:X,Y:] = Y

A4: now

let y be set ; :: thesis: ( y in Y implies ex x being set st [x,y] in [:X,Y:] )
assume y in Y ; :: thesis: ex x being set st [x,y] in [:X,Y:]
then [a,y] in [:X,Y:] by A1, ZFMISC_1:87;
hence ex x being set st [x,y] in [:X,Y:] ; :: thesis: verum

end;

for y being set st ex x being set st [x,y] in [:X,Y:] holds
y in Y by ZFMISC_1:87;
hence rng [:X,Y:] = Y by A4, Def5; :: thesis: verum