let X, Y be set ; :: thesis: ( ( Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} ) implies ( proj1 [:X,Y:] = X & proj2 [:Y,X:] = X ) )
set y = the Element of Y;
assume ( Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} ) ; :: thesis: ( proj1 [:X,Y:] = X & proj2 [:Y,X:] = X )
then A1: Y <> {} by ZFMISC_1:90;

now :: thesis: for x being object holds
( x in X iff ex y being object st [x,y] in [:X,Y:] )

let x be object ; :: thesis: ( x in X iff ex y being object st [x,y] in [:X,Y:] )
( x in X implies [x, the Element of Y] in [:X,Y:] ) by A1, ZFMISC_1:87;
hence ( x in X iff ex y being object st [x,y] in [:X,Y:] ) by ZFMISC_1:87; :: thesis: verum

end;

hence proj1 [:X,Y:] = X by XTUPLE_0:def 12; :: thesis: proj2 [:Y,X:] = X

now :: thesis: for x being object holds
( x in X iff ex y being object st [y,x] in [:Y,X:] )

let x be object ; :: thesis: ( x in X iff ex y being object st [y,x] in [:Y,X:] )
( x in X implies [ the Element of Y,x] in [:Y,X:] ) by A1, ZFMISC_1:87;
hence ( x in X iff ex y being object st [y,x] in [:Y,X:] ) by ZFMISC_1:87; :: thesis: verum

end;

hence proj2 [:Y,X:] = X by XTUPLE_0:def 13; :: thesis: verum