theorem
Th45
:
:: MONOID_1:45
for
D1
,
D2
,
D
being non
empty
set
for
f
being
Function
of
[:
D1
,
D2
:]
,
D
for
X1
being
Subset
of
D1
for
X2
being
Subset
of
D2
for
x1
,
x2
being
set
st
x1
in
X1
&
x2
in
X2
holds
f
.
(
x1
,
x2
)
in
(
f
.:^2
)
.
(
X1
,
X2
)