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 object 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 object such that
A2: b in Y by XBOOLE_0:def 1;
A3: now :: thesis: for x being object st x in X holds
ex y being object st [x,y] in [:X,Y:]
let x be object ; :: thesis: ( x in X implies ex y being object st [x,y] in [:X,Y:] )
assume x in X ; :: thesis: ex y being object st [x,y] in [:X,Y:]
then [x,b] in [:X,Y:] by A2, ZFMISC_1:87;
hence ex y being object st [x,y] in [:X,Y:] ; :: thesis: verum
end;
for x being object st ex y being object st [x,y] in [:X,Y:] holds
x in X by ZFMISC_1:87;
hence dom [:X,Y:] = X by A3, XTUPLE_0:def 12; :: thesis: rng [:X,Y:] = Y
A4: now :: thesis: for y being object st y in Y holds
ex x being object st [x,y] in [:X,Y:]
let y be object ; :: thesis: ( y in Y implies ex x being object st [x,y] in [:X,Y:] )
assume y in Y ; :: thesis: ex x being object st [x,y] in [:X,Y:]
then [a,y] in [:X,Y:] by A1, ZFMISC_1:87;
hence ex x being object st [x,y] in [:X,Y:] ; :: thesis: verum
end;
for y being object st ex x being object st [x,y] in [:X,Y:] holds
y in Y by ZFMISC_1:87;
hence rng [:X,Y:] = Y by A4, XTUPLE_0:def 13; :: thesis: verum