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 st r <> 0 holds
( F,G are_fiberwise_equipotent iff r (#) F,r (#) G are_fiberwise_equipotent )
let F be PartFunc of D,REAL; :: thesis: 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; :: thesis: 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; :: thesis: ( r <> 0 implies ( F,G are_fiberwise_equipotent iff r (#) F,r (#) G are_fiberwise_equipotent ) )
assume A1: r <> 0 ; :: thesis: ( 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 ) :: thesis: ( r (#) F,r (#) G are_fiberwise_equipotent implies F,G are_fiberwise_equipotent )

proof

assume A3: F,G are_fiberwise_equipotent ; :: thesis: r (#) F,r (#) G are_fiberwise_equipotent

now :: thesis: for x being Element of REAL holds card (Coim ((r (#) F),x)) = card (Coim ((r (#) G),x))

let x be Element of REAL ; :: thesis: 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; :: thesis: verum

end;

hence r (#) F,r (#) G are_fiberwise_equipotent by A2, CLASSES1:79; :: thesis: verum

end;

assume A4: r (#) F,r (#) G are_fiberwise_equipotent ; :: thesis: F,G are_fiberwise_equipotent

A5: now :: thesis: for x being Element of REAL holds card (Coim (F,x)) = card (Coim (G,x))

let x be Element of REAL ; :: thesis: 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; :: thesis: verum

end;

( rng F c= REAL & rng G c= REAL ) ;
hence F,G are_fiberwise_equipotent by A5, CLASSES1:79; :: thesis: verum