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 )
A2: ( rng (r (#) F) c= REAL & rng (r (#) 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

let x be 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, Th8;
hence card (Coim (r (#) F),x) = card (Coim (r (#) G),x) by A3, CLASSES1:def 9; :: thesis: verum

end;

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

end;

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

A5: now

let x be Real; :: thesis: card (Coim F,x) = card (Coim G,x)
A6: G " {((r * x) / r)} = Coim (r (#) G),(r * x) by A1, Th8;
( (r * x) / r = x & F " {((r * x) / r)} = Coim (r (#) F),(r * x) ) by A1, Th8, XCMPLX_1:90;
hence card (Coim F,x) = card (Coim G,x) by A4, A6, CLASSES1:def 9; :: thesis: verum

end;

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