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 A1: ( max+ F, max+ G are_fiberwise_equipotent & max- F, max- G are_fiberwise_equipotent ) ; :: thesis: F,G are_fiberwise_equipotent
A2: ( rng F c= REAL & rng G c= REAL & rng (max+ F) c= REAL & rng (max- F) c= REAL & rng (max+ G) c= REAL & rng (max- G) c= REAL ) ;
A3: ( dom F = dom (max+ F) & dom F = dom (max- F) & dom G = dom (max+ G) & dom G = dom (max- G) ) by Def10, Def11;
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 };
A4: (left_closed_halfline 0 ) /\ (right_closed_halfline 0 ) = [.0 ,0 .] by XXREAL_1:272
.= {0 } by XXREAL_1:17 ;
A5: ( F " (left_closed_halfline 0 ) = (max+ F) " {0 } & F " (right_closed_halfline 0 ) = (max- F) " {0 } & 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 ;
( 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 A6: ( card (fp0 /\ fm0) = ((card fp0) + (card fm0)) - (card (fp0 \/ fm0)) & card (gp0 /\ gm0) = ((card gp0) + (card gm0)) - (card (gp0 \/ gm0)) ) ;
A7: (left_closed_halfline 0 ) \/ (right_closed_halfline 0 ) = REAL \ ].0 ,0 .[ by XXREAL_1:398
.= REAL \ {} by XXREAL_1:28
.= REAL ;
then A8: fp0 \/ fm0 = F " REAL by A5, RELAT_1:175;
F " (rng F) c= F " REAL by RELAT_1:178;
then ( F " REAL c= dom F & dom F c= F " REAL ) by RELAT_1:167, RELAT_1:169;
then A9: fp0 \/ fm0 = dom F by A8, XBOOLE_0:def 10;
A10: gp0 \/ gm0 = G " ((left_closed_halfline 0 ) \/ (right_closed_halfline 0 )) by A5, RELAT_1:175;
G " (rng G) c= G " REAL by RELAT_1:178;
then ( G " REAL c= dom G & dom G c= G " REAL ) by RELAT_1:167, RELAT_1:169;
then A11: gp0 \/ gm0 = dom G by A7, A10, XBOOLE_0:def 10;

now

let r be Real; :: thesis: card (Coim F,r) = card (Coim G,r)
A12: ( card fp0 = card gp0 & card fm0 = card gm0 ) by A1, 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 A4, FUNCT_1:137;
hence card (F " {r}) = card (G " {r}) by A1, A3, A5, A6, A9, A11, A12, CLASSES1:89; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

hence F,G are_fiberwise_equipotent by A2, CLASSES1:87; :: thesis: verum