set li = right_closed_halfline 0;
let D, C be non empty set ; :: thesis: for F being PartFunc of D,REAL
for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds
max- F, max- G are_fiberwise_equipotent
let F be PartFunc of D,REAL; :: thesis: for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds
max- F, max- G are_fiberwise_equipotent
let G be PartFunc of C,REAL; :: 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 :: thesis: for r being Element of REAL holds card (Coim ((max- F),r)) = card (Coim ((max- G),r))

let r be Element of REAL ; :: thesis: card (Coim ((max- F),r)) = card (Coim ((max- G),r))

now :: thesis: ( ( 0 < r & card (Coim ((max- F),r)) = card (Coim ((max- G),r)) ) or ( r = 0 & card ((max- F) " {r}) = card ((max- G) " {r}) ) or ( r < 0 & card ((max- F) " {r}) = card ((max- G) " {r}) ) )

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)) = (max- F) " {r} & Coim (G,(- r)) = (max- G) " {r} ) by Th38;
hence card (Coim ((max- F),r)) = card (Coim ((max- G),r)) by A1, CLASSES1:def 10; :: thesis: verum

end;

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

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

end;

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

now :: thesis: not r in rng (max- F)

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:3;
hence contradiction by A4, Th40; :: thesis: verum

end;

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

now :: thesis: not r in rng (max- G)

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:3;
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:79; :: thesis: verum