theorem :: RFUNCT_3:43

for D, C being non empty set
for F being finite PartFunc of D,REAL
for G being finite PartFunc of C,REAL st max+ F, max+ G are_fiberwise_equipotent & max- F, max- G are_fiberwise_equipotent holds
F,G are_fiberwise_equipotent