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:143;
then A4: ( F " REAL c= dom F & dom F c= F " REAL ) by RELAT_1:132, RELAT_1:134;
A5: ( F " (left_closed_halfline 0) = (max+ F) " {0} & F " (right_closed_halfline 0) = (max- F) " {0} ) by Th36, Th39;
G " (rng G) c= G " REAL by RELAT_1:143;
then A6: ( G " REAL c= dom G & dom G c= G " REAL ) by RELAT_1:132, RELAT_1:134;
A7: ( G " (left_closed_halfline 0) = (max+ G) " {0} & G " (right_closed_halfline 0) = (max- G) " {0} ) by Th36, Th39;
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:140;
then A9: fp0 \/ fm0 = dom F by A4;
gp0 \/ gm0 = G " ((left_closed_halfline 0) \/ (right_closed_halfline 0)) by A7, RELAT_1:140;
then A10: gp0 \/ gm0 = dom G by A8, A6;
card (fp0 \/ fm0) = ((card fp0) + (card fm0)) - (card (fp0 /\ fm0)) by CARD_2:45;
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:45;
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 :: thesis: for r being Element of REAL holds card (Coim (F,r)) = card (Coim (G,r))
let r be Element of REAL ; :: thesis: card (Coim (F,r)) = card (Coim (G,r))
A15: ( card fp0 = card gp0 & card fm0 = card gm0 ) by A1, A2, CLASSES1:78;
now :: thesis: ( ( 0 < r & card (Coim (F,r)) = card (Coim (G,r)) ) or ( 0 = r & card (F " {r}) = card (G " {r}) ) or ( r < 0 & card (Coim (F,r)) = card (Coim (G,r)) ) )
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 Th35;
hence card (Coim (F,r)) = card (Coim (G,r)) by A1, CLASSES1:def 10; :: 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:58;
then ( Coim (F,r) = Coim ((max- F),(- r)) & Coim (G,r) = Coim ((max- G),(- r)) ) by A17, Th38;
hence card (Coim (F,r)) = card (Coim (G,r)) by A2, CLASSES1:def 10; :: 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:79; :: thesis: verum