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 Th9
.= X1 by A1, Th12 ; :: thesis: (.: (pr2 X,Y)) . [:X1,Y1:] = Y1
thus (.: (pr2 X,Y)) . [:X1,Y1:] = (pr2 X,Y) .: [:X1,Y1:] by Th10
.= Y1 by A1, Th12 ; :: thesis: verum