set li = left_closed_halfline 0 ;
let D, C be non empty set ; :: thesis: for F being PartFunc of ,
for G being PartFunc of , st F,G are_fiberwise_equipotent holds
max+ F, max+ G are_fiberwise_equipotent
let F be PartFunc of ,; :: thesis: for G being PartFunc of , st F,G are_fiberwise_equipotent holds
max+ F, max+ G are_fiberwise_equipotent
let G be PartFunc of ,; :: thesis: ( F,G are_fiberwise_equipotent implies max+ F, max+ G are_fiberwise_equipotent )
assume A1: F,G are_fiberwise_equipotent ; :: thesis: max+ F, max+ G are_fiberwise_equipotent

A2: now

let r be Real; :: thesis: card (Coim (max+ F),r) = card (Coim (max+ G),r)

now

per cases ( 0 < r or r = 0 or r < 0 ) ;

case 0 < r ; :: thesis: card (Coim (max+ F),r) = card (Coim (max+ G),r)

then ( Coim F,r = Coim (max+ F),r & Coim G,r = Coim (max+ G),r ) by Th38;
hence card (Coim (max+ F),r) = card (Coim (max+ G),r) by A1, CLASSES1:def 9; :: thesis: verum

end;

case A3: r = 0 ; :: thesis: card ((max+ F) " {r}) = card ((max+ G) " {r})

( F " (left_closed_halfline 0 ) = (max+ F) " {0 } & G " (left_closed_halfline 0 ) = (max+ G) " {0 } ) by Th39;
hence card ((max+ F) " {r}) = card ((max+ G) " {r}) by A1, A3, CLASSES1:86; :: thesis: verum

end;

case A4: r < 0 ; :: thesis: card ((max+ F) " {r}) = card ((max+ G) " {r})

now

assume r in rng (max+ F) ; :: thesis: contradiction
then ex d being Element of D st
( d in dom (max+ F) & (max+ F) . d = r ) by PARTFUN1:26;
hence contradiction by A4, Th40; :: thesis: verum

end;

then A5: (max+ F) " {r} = {} by Lm2;

now

assume r in rng (max+ G) ; :: thesis: contradiction
then ex c being Element of C st
( c in dom (max+ G) & (max+ G) . c = r ) by PARTFUN1:26;
hence contradiction by A4, Th40; :: thesis: verum

end;

hence card ((max+ F) " {r}) = card ((max+ G) " {r}) by A5, Lm2; :: thesis: verum

end;

end;

end;

hence card (Coim (max+ F),r) = card (Coim (max+ G),r) ; :: thesis: verum

end;

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