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 & - G = (- 1) (#) G ) ;
hence ( F,G are_fiberwise_equipotent iff - F, - G are_fiberwise_equipotent ) by Th13; :: thesis: verum