let X, Y be set ; :: thesis: for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
let X1 be Subset of X; :: thesis: for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
let Y1 be Subset of Y; :: thesis: ( [:X1,Y1:] <> {} implies ( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 ) )
assume A1: [:X1,Y1:] <> {} ; :: thesis: ( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
then A2: X1 <> {} ;
A3: Y1 <> {} by A1;
A4: X <> {} by A2;

now :: thesis: for x being object holds
( ( x in (pr1 (X,Y)) .: [:X1,Y1:] implies x in X1 ) & ( x in X1 implies x in (pr1 (X,Y)) .: [:X1,Y1:] ) )

set y = the Element of Y1;
let x be object ; :: thesis: ( ( x in (pr1 (X,Y)) .: [:X1,Y1:] implies x in X1 ) & ( x in X1 implies x in (pr1 (X,Y)) .: [:X1,Y1:] ) )
thus ( x in (pr1 (X,Y)) .: [:X1,Y1:] implies x in X1 ) :: thesis: ( x in X1 implies x in (pr1 (X,Y)) .: [:X1,Y1:] )

proof

assume x in (pr1 (X,Y)) .: [:X1,Y1:] ; :: thesis: x in X1
then consider u being object such that
A5: u in [:X,Y:] and
A6: ( u in [:X1,Y1:] & x = (pr1 (X,Y)) . u ) by FUNCT_2:64;
A7: u `2 in Y by A5, MCART_1:10;
( u `1 in X1 & x = (pr1 (X,Y)) . ((u `1),(u `2)) ) by A6, MCART_1:10, MCART_1:21;
hence x in X1 by A7, FUNCT_3:def 4; :: thesis: verum

end;

assume A8: x in X1 ; :: thesis: x in (pr1 (X,Y)) .: [:X1,Y1:]
the Element of Y1 in Y by A3, TARSKI:def 3;
then A9: x = (pr1 (X,Y)) . (x, the Element of Y1) by A8, FUNCT_3:def 4;
[x, the Element of Y1] in [:X1,Y1:] by A3, A8, ZFMISC_1:87;
hence x in (pr1 (X,Y)) .: [:X1,Y1:] by A4, A9, FUNCT_2:35; :: thesis: verum

end;

hence (pr1 (X,Y)) .: [:X1,Y1:] = X1 by TARSKI:2; :: thesis: (pr2 (X,Y)) .: [:X1,Y1:] = Y1
A10: Y <> {} by A3;

now :: thesis: for y being object holds
( ( y in (pr2 (X,Y)) .: [:X1,Y1:] implies y in Y1 ) & ( y in Y1 implies y in (pr2 (X,Y)) .: [:X1,Y1:] ) )

set x = the Element of X1;
let y be object ; :: thesis: ( ( y in (pr2 (X,Y)) .: [:X1,Y1:] implies y in Y1 ) & ( y in Y1 implies y in (pr2 (X,Y)) .: [:X1,Y1:] ) )
thus ( y in (pr2 (X,Y)) .: [:X1,Y1:] implies y in Y1 ) :: thesis: ( y in Y1 implies y in (pr2 (X,Y)) .: [:X1,Y1:] )

proof

assume y in (pr2 (X,Y)) .: [:X1,Y1:] ; :: thesis: y in Y1
then consider u being object such that
A11: u in [:X,Y:] and
A12: ( u in [:X1,Y1:] & y = (pr2 (X,Y)) . u ) by FUNCT_2:64;
A13: u `1 in X by A11, MCART_1:10;
( u `2 in Y1 & y = (pr2 (X,Y)) . ((u `1),(u `2)) ) by A12, MCART_1:10, MCART_1:21;
hence y in Y1 by A13, FUNCT_3:def 5; :: thesis: verum

end;

assume A14: y in Y1 ; :: thesis: y in (pr2 (X,Y)) .: [:X1,Y1:]
the Element of X1 in X by A2, TARSKI:def 3;
then A15: y = (pr2 (X,Y)) . ( the Element of X1,y) by A14, FUNCT_3:def 5;
[ the Element of X1,y] in [:X1,Y1:] by A2, A14, ZFMISC_1:87;
hence y in (pr2 (X,Y)) .: [:X1,Y1:] by A10, A15, FUNCT_2:35; :: thesis: verum

end;

hence (pr2 (X,Y)) .: [:X1,Y1:] = Y1 by TARSKI:2; :: thesis: verum