let D, C be non empty set ; :: thesis: for F being PartFunc of ,
for G being PartFunc of , holds
( F,G are_fiberwise_equipotent iff - F, - G are_fiberwise_equipotent )
let F be PartFunc of ,; :: thesis: for G being PartFunc of , holds
( F,G are_fiberwise_equipotent iff - F, - G are_fiberwise_equipotent )
let G be PartFunc of ,; :: 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