theorem
for
S,
T being non
empty RelStr for
f being
set holds
( (
f is
Function of
S,
T implies
f is
Function of
(S opp),
T ) & (
f is
Function of
(S opp),
T implies
f is
Function of
S,
T ) & (
f is
Function of
S,
T implies
f is
Function of
S,
(T opp) ) & (
f is
Function of
S,
(T opp) implies
f is
Function of
S,
T ) & (
f is
Function of
S,
T implies
f is
Function of
(S opp),
(T opp) ) & (
f is
Function of
(S opp),
(T opp) implies
f is
Function of
S,
T ) ) ;