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 )

thus (.: (pr1 (X,Y))) . [:X1,Y1:] = (pr1 (X,Y)) .: [:X1,Y1:] by Th47

.= X1 by A1, Th49 ; :: thesis: (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1

thus (.: (pr2 (X,Y))) . [:X1,Y1:] = (pr2 (X,Y)) .: [:X1,Y1:] by Th48

.= Y1 by A1, Th49 ; :: thesis: verum

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 )

thus (.: (pr1 (X,Y))) . [:X1,Y1:] = (pr1 (X,Y)) .: [:X1,Y1:] by Th47

.= X1 by A1, Th49 ; :: thesis: (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1

thus (.: (pr2 (X,Y))) . [:X1,Y1:] = (pr2 (X,Y)) .: [:X1,Y1:] by Th48

.= Y1 by A1, Th49 ; :: thesis: verum