set li = left_closed_halfline 0;
let D, C be non empty set ; :: thesis:
let F be PartFunc of D,REAL; :: thesis:
let G be PartFunc of C,REAL; :: thesis:
assume A1: F,G are_fiberwise_equipotent ; :: thesis:

A2: now :: thesis:

let r be Element of REAL ; :: thesis:

case 0 < r ; :: thesis:

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

end;

case A3: r = 0 ; :: thesis:

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

end;

case A4: r < 0 ; :: thesis:

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

end;

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

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

end;

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

end;

end;

end;

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

end;

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