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 [:X1,Y1:] <> {} ; :: thesis: ( (pr1 X,Y) .: [:X1,Y1:] = X1 & (pr2 X,Y) .: [:X1,Y1:] = Y1 )
then A1: ( X1 <> {} & Y1 <> {} & X1 c= X & Y1 c= Y ) by ZFMISC_1:113;
then A2: ( X <> {} & Y <> {} ) ;

now

let x be set ; :: 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 set such that
A3: ( u in [:X,Y:] & u in [:X1,Y1:] & x = (pr1 X,Y) . u ) by FUNCT_2:115;
A4: u `1 in X1 by A3, MCART_1:10;
A5: x = (pr1 X,Y) . (u `1 ),(u `2 ) by A3, MCART_1:23;
( u `1 in X & u `2 in Y ) by A3, MCART_1:10;
hence x in X1 by A4, A5, FUNCT_3:def 5; :: thesis: verum

end;

consider y being Element of Y1;
assume A6: x in X1 ; :: thesis: x in (pr1 X,Y) .: [:X1,Y1:]
then A7: ( x in X & y in Y ) by A1, TARSKI:def 3;
A8: [x,y] in [:X1,Y1:] by A1, A6, ZFMISC_1:106;
x = (pr1 X,Y) . x,y by A7, FUNCT_3:def 5;
hence x in (pr1 X,Y) .: [:X1,Y1:] by A2, A8, FUNCT_2:43; :: thesis: verum

end;

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

now

let y be set ; :: 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 set such that
A9: ( u in [:X,Y:] & u in [:X1,Y1:] & y = (pr2 X,Y) . u ) by FUNCT_2:115;
A10: u `2 in Y1 by A9, MCART_1:10;
A11: y = (pr2 X,Y) . (u `1 ),(u `2 ) by A9, MCART_1:23;
( u `1 in X & u `2 in Y ) by A9, MCART_1:10;
hence y in Y1 by A10, A11, FUNCT_3:def 6; :: thesis: verum

end;

consider x being Element of X1;
assume A12: y in Y1 ; :: thesis: y in (pr2 X,Y) .: [:X1,Y1:]
then A13: ( x in X & y in Y ) by A1, TARSKI:def 3;
A14: [x,y] in [:X1,Y1:] by A1, A12, ZFMISC_1:106;
y = (pr2 X,Y) . x,y by A13, FUNCT_3:def 6;
hence y in (pr2 X,Y) .: [:X1,Y1:] by A2, A14, FUNCT_2:43; :: thesis: verum

end;

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