let D, C be non empty set ; :: thesis: for F being finite PartFunc of D,REAL
for G being finite PartFunc of C,REAL st max+ F, max+ G are_fiberwise_equipotent & max- F, max- G are_fiberwise_equipotent holds
F,G are_fiberwise_equipotent
let F be finite PartFunc of D,REAL ; :: thesis: for G being finite PartFunc of C,REAL st max+ F, max+ G are_fiberwise_equipotent & max- F, max- G are_fiberwise_equipotent holds
F,G are_fiberwise_equipotent
let G be finite PartFunc of C,REAL ; :: thesis: ( max+ F, max+ G are_fiberwise_equipotent & max- F, max- G are_fiberwise_equipotent implies F,G are_fiberwise_equipotent )
assume that
A1: max+ F, max+ G are_fiberwise_equipotent and
A2: max- F, max- G are_fiberwise_equipotent ; :: thesis: F,G are_fiberwise_equipotent
set lh = left_closed_halfline 0 ;
set rh = right_closed_halfline 0 ;
set fp0 = (max+ F) " {0 };
set fm0 = (max- F) " {0 };
set gp0 = (max+ G) " {0 };
set gm0 = (max- G) " {0 };
A3: (left_closed_halfline 0 ) /\ (right_closed_halfline 0 ) = [.0 ,0 .] by XXREAL_1:272
.= {0 } by XXREAL_1:17 ;
F " (rng F) c= F " REAL by RELAT_1:178;
then A4: ( F " REAL c= dom F & dom F c= F " REAL ) by RELAT_1:167, RELAT_1:169;
A5: ( F " (left_closed_halfline 0 ) = (max+ F) " {0 } & F " (right_closed_halfline 0 ) = (max- F) " {0 } ) by Th39, Th42;
G " (rng G) c= G " REAL by RELAT_1:178;
then A6: ( G " REAL c= dom G & dom G c= G " REAL ) by RELAT_1:167, RELAT_1:169;
A7: ( G " (left_closed_halfline 0 ) = (max+ G) " {0 } & G " (right_closed_halfline 0 ) = (max- G) " {0 } ) by Th39, Th42;
reconsider fp0 = (max+ F) " {0 }, fm0 = (max- F) " {0 }, gp0 = (max+ G) " {0 }, gm0 = (max- G) " {0 } as finite set ;
A8: (left_closed_halfline 0 ) \/ (right_closed_halfline 0 ) = REAL \ ].0 ,0 .[ by XXREAL_1:398
.= REAL \ {} by XXREAL_1:28
.= REAL ;
then fp0 \/ fm0 = F " REAL by A5, RELAT_1:175;
then A9: fp0 \/ fm0 = dom F by A4, XBOOLE_0:def 10;
gp0 \/ gm0 = G " ((left_closed_halfline 0 ) \/ (right_closed_halfline 0 )) by A7, RELAT_1:175;
then A10: gp0 \/ gm0 = dom G by A8, A6, XBOOLE_0:def 10;
card (fp0 \/ fm0) = ((card fp0) + (card fm0)) - (card (fp0 /\ fm0)) by CARD_2:64;
then A11: card (fp0 /\ fm0) = ((card fp0) + (card fm0)) - (card (fp0 \/ fm0)) ;
card (gp0 \/ gm0) = ((card gp0) + (card gm0)) - (card (gp0 /\ gm0)) by CARD_2:64;
then A12: card (gp0 /\ gm0) = ((card gp0) + (card gm0)) - (card (gp0 \/ gm0)) ;
A13: ( dom F = dom (max+ F) & dom G = dom (max+ G) ) by Def10;

A14: now

let r be Real; :: thesis: card (Coim F,r) = card (Coim G,r)
A15: ( card fp0 = card gp0 & card fm0 = card gm0 ) by A1, A2, CLASSES1:86;

now

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

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

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

end;

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

then ( F " {r} = (F " (left_closed_halfline 0 )) /\ (F " (right_closed_halfline 0 )) & G " {r} = (G " (left_closed_halfline 0 )) /\ (G " (right_closed_halfline 0 )) ) by A3, FUNCT_1:137;
hence card (F " {r}) = card (G " {r}) by A1, A13, A5, A7, A11, A12, A9, A10, A15, CLASSES1:89; :: thesis: verum

end;

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

A17: - (- r) = r ;
0 < - r by A16, XREAL_1:60;
then ( Coim F,r = Coim (max- F),(- r) & Coim G,r = Coim (max- G),(- r) ) by A17, Th41;
hence card (Coim F,r) = card (Coim G,r) by A2, CLASSES1:def 9; :: thesis: verum

end;

end;

end;

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

end;

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