let D, C be non empty set ; for F being PartFunc of D,REAL
for G being PartFunc of C,REAL
for r being Real holds
( F,G are_fiberwise_equipotent iff F - r,G - r are_fiberwise_equipotent )
let F be PartFunc of D,REAL; for G being PartFunc of C,REAL
for r being Real holds
( F,G are_fiberwise_equipotent iff F - r,G - r are_fiberwise_equipotent )
let G be PartFunc of C,REAL; for r being Real holds
( F,G are_fiberwise_equipotent iff F - r,G - r are_fiberwise_equipotent )
let r be Real; ( F,G are_fiberwise_equipotent iff F - r,G - r are_fiberwise_equipotent )
A1:
( rng (F - r) c= REAL & rng (G - r) c= REAL )
;
thus
( F,G are_fiberwise_equipotent implies F - r,G - r are_fiberwise_equipotent )
( F - r,G - r are_fiberwise_equipotent implies F,G are_fiberwise_equipotent )
assume A3:
F - r,G - r are_fiberwise_equipotent
; F,G are_fiberwise_equipotent
( rng F c= REAL & rng G c= REAL )
;
hence
F,G are_fiberwise_equipotent
by A4, CLASSES1:79; verum