thus
for
f
,
g
being
Function
of
[:
I[01]
,
I[01]
:]
,
T
st ( for
a
,
b
being
Point
of
I[01]
holds
f
.
(
a
,
b
)
=
H
_{1}
(
a
,
b
) ) & ( for
a
,
b
being
Point
of
I[01]
holds
g
.
(
a
,
b
)
=
H
_{1}
(
a
,
b
) ) holds
f
=
g
from
TOPALG_7:sch 2
();
:: thesis:
verum