let X, Y be set ; 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; 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; ( [:X1,Y1:] <> {} implies ( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 & (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 ) )
assume A1:
[:X1,Y1:] <> {}
; ( (.: (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
; (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1
thus (.: (pr2 (X,Y))) . [:X1,Y1:] =
(pr2 (X,Y)) .: [:X1,Y1:]
by Th48
.=
Y1
by A1, Th49
; verum