theorem Th1:
for
A,
O being non
empty set for
R being
Order of
A for
Ol being
Equivalence_Relation of
O for
f being
Function of
O,
(A *) for
g being
Function of
O,
A holds
( not
OverloadedRSSign(#
A,
R,
O,
Ol,
f,
g #) is
empty & not
OverloadedRSSign(#
A,
R,
O,
Ol,
f,
g #) is
void &
OverloadedRSSign(#
A,
R,
O,
Ol,
f,
g #) is
reflexive &
OverloadedRSSign(#
A,
R,
O,
Ol,
f,
g #) is
transitive &
OverloadedRSSign(#
A,
R,
O,
Ol,
f,
g #) is
antisymmetric )