let D, C be non empty set ; :: thesis:
let F be PartFunc of D,REAL; :: thesis:
let G be PartFunc of C,REAL; :: thesis:
let r be Real; :: thesis:
assume A1: r <> 0 ; :: thesis:
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:

proof

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

now :: thesis:

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

end;

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

end;

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

A5: now :: thesis:

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

end;

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