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;

A10: Y <> {} by A3;

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:] ) )

hence
(pr1 (X,Y)) .: [:X1,Y1:] = X1
by TARSKI:2; :: thesis: (pr2 (X,Y)) .: [:X1,Y1:] = Y1( ( 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:] )

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;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 A8:
x in X1
; :: thesis: x in (pr1 (X,Y)) .: [:X1,Y1:]
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;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

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

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:] ) )

hence
(pr2 (X,Y)) .: [:X1,Y1:] = Y1
by TARSKI:2; :: thesis: verum( ( 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:] )

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;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 A14:
y in Y1
; :: thesis: y in (pr2 (X,Y)) .: [:X1,Y1:]
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;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

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