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 st r <> 0 holds
( F,G are_fiberwise_equipotent iff r (#) F,r (#) G are_fiberwise_equipotent )
let F be PartFunc of D,REAL; for G being PartFunc of C,REAL
for r being Real st r <> 0 holds
( F,G are_fiberwise_equipotent iff r (#) F,r (#) G are_fiberwise_equipotent )
let G be PartFunc of C,REAL; for r being Real st r <> 0 holds
( F,G are_fiberwise_equipotent iff r (#) F,r (#) G are_fiberwise_equipotent )
let r be Real; ( r <> 0 implies ( F,G are_fiberwise_equipotent iff r (#) F,r (#) G are_fiberwise_equipotent ) )
assume A1:
r <> 0
; ( F,G are_fiberwise_equipotent iff r (#) F,r (#) G are_fiberwise_equipotent )
reconsider rr = r as Element of REAL by XREAL_0:def 1;
A2:
( rng (rr (#) F) c= REAL & rng (rr (#) G) c= REAL )
;
thus
( F,G are_fiberwise_equipotent implies r (#) F,r (#) G are_fiberwise_equipotent )
( r (#) F,r (#) G are_fiberwise_equipotent implies F,G are_fiberwise_equipotent )proof
assume A3:
F,
G are_fiberwise_equipotent
;
r (#) F,r (#) G are_fiberwise_equipotent
now for x being Element of REAL holds card (Coim ((r (#) F),x)) = card (Coim ((r (#) G),x))let x be
Element of
REAL ;
card (Coim ((r (#) F),x)) = card (Coim ((r (#) G),x))
(
Coim (
F,
(x / r))
= Coim (
(r (#) F),
x) &
Coim (
G,
(x / r))
= Coim (
(r (#) G),
x) )
by A1, Th6;
hence
card (Coim ((r (#) F),x)) = card (Coim ((r (#) G),x))
by A3, CLASSES1:def 10;
verum end;
hence
r (#) F,
r (#) G are_fiberwise_equipotent
by A2, CLASSES1:79;
verum
end;
assume A4:
r (#) F,r (#) G are_fiberwise_equipotent
; F,G are_fiberwise_equipotent
A5:
now for x being Element of REAL holds card (Coim (F,x)) = card (Coim (G,x))let x be
Element of
REAL ;
card (Coim (F,x)) = card (Coim (G,x))A6:
G " {((r * x) / r)} = Coim (
(r (#) G),
(r * x))
by A1, Th6;
(
(r * x) / r = x &
F " {((r * x) / r)} = Coim (
(r (#) F),
(r * x)) )
by A1, Th6, XCMPLX_1:89;
hence
card (Coim (F,x)) = card (Coim (G,x))
by A4, A6, CLASSES1:def 10;
verum end;
( rng F c= REAL & rng G c= REAL )
;
hence
F,G are_fiberwise_equipotent
by A5, CLASSES1:79; verum