let D, C be non empty set ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: for r being Real holds
( F,G are_fiberwise_equipotent iff F - r,G - r are_fiberwise_equipotent )
let r be Real; :: thesis: ( F,G are_fiberwise_equipotent iff F - r,G - r are_fiberwise_equipotent )
A1: ( rng F c= REAL & rng G c= REAL & rng (F - r) c= REAL & rng (G - r) c= REAL ) ;
thus ( F,G are_fiberwise_equipotent implies F - r,G - r are_fiberwise_equipotent ) :: thesis: ( F - r,G - r are_fiberwise_equipotent implies F,G are_fiberwise_equipotent )

proof

assume A2: F,G are_fiberwise_equipotent ; :: thesis: F - r,G - r are_fiberwise_equipotent

now

let s be Real; :: thesis: card (Coim (F - r),s) = card (Coim (G - r),s)
thus card (Coim (F - r),s) = card (Coim F,(s + r)) by Th53
.= card (Coim G,(s + r)) by A2, CLASSES1:def 9
.= card (Coim (G - r),s) by Th53 ; :: thesis: verum

end;

hence F - r,G - r are_fiberwise_equipotent by A1, CLASSES1:87; :: thesis: verum

end;

assume A3: F - r,G - r are_fiberwise_equipotent ; :: thesis: F,G are_fiberwise_equipotent

now

let s be Real; :: thesis: card (Coim F,s) = card (Coim G,s)
A4: s = (s - r) + r ;
hence card (Coim F,s) = card (Coim (F - r),(s - r)) by Th53
.= card (Coim (G - r),(s - r)) by A3, CLASSES1:def 9
.= card (Coim G,s) by A4, Th53 ;
:: thesis: verum

end;

hence F,G are_fiberwise_equipotent by A1, CLASSES1:87; :: thesis: verum