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 ) ) ;