let D, C be non empty set ; :: thesis: for F being PartFunc of D,REAL
for G being PartFunc of C,REAL holds
( F,G are_fiberwise_equipotent iff - F, - G are_fiberwise_equipotent )
let F be PartFunc of D,REAL ; :: thesis: for G being PartFunc of C,REAL holds
( F,G are_fiberwise_equipotent iff - F, - G are_fiberwise_equipotent )
let G be PartFunc of C,REAL ; :: thesis: ( F,G are_fiberwise_equipotent iff - F, - G are_fiberwise_equipotent )
- F = (- 1) (#) F ;
hence ( F,G are_fiberwise_equipotent iff - F, - G are_fiberwise_equipotent ) by Th13; :: thesis: verum