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