theorem
Th44
:
:: MONOID_1:44
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
holds
(
f
.:^2
)
.
(
X1
,
X2
)
=
f
.:
[:
X1
,
X2
:]