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 - 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 :: thesis: for s being Element of REAL holds card (Coim ((F - r),s)) = card (Coim ((G - r),s))
let s be Element of REAL ; :: thesis: card (Coim ((F - r),s)) = card (Coim ((G - r),s))
thus card (Coim ((F - r),s)) = card (Coim (F,(s + r))) by Th50
.= card (Coim (G,(s + r))) by A2, CLASSES1:def 10
.= card (Coim ((G - r),s)) by Th50 ; :: thesis: verum
end;
hence F - r,G - r are_fiberwise_equipotent by A1, CLASSES1:79; :: thesis: verum
end;
assume A3: F - r,G - r are_fiberwise_equipotent ; :: thesis: F,G are_fiberwise_equipotent
A4: now :: thesis: for s being Element of REAL holds card (Coim (F,s)) = card (Coim (G,s))
let s be Element of REAL ; :: thesis: card (Coim (F,s)) = card (Coim (G,s))
A5: s = (s - r) + r ;
hence card (Coim (F,s)) = card (Coim ((F - r),(s - r))) by Th50
.= card (Coim ((G - r),(s - r))) by A3, CLASSES1:def 10
.= card (Coim (G,s)) by A5, Th50 ;
:: thesis: verum
end;
( rng F c= REAL & rng G c= REAL ) ;
hence F,G are_fiberwise_equipotent by A4, CLASSES1:79; :: thesis: verum