let A be set ; :: thesis:
let S be finite Subset of A; :: thesis:
let b be Rbag of A; :: thesis:
assume A1: support b c= S ; :: thesis:
A2: card (support b) <= card S by A1, NAT_1:43;
set cs = canFS (support b);
A3: rng (canFS (support b)) = support b by FUNCT_2:def 3;
set cS = canFS S;
set f = b * (canFS S);
len (canFS S) = card S by FINSEQ_1:93;
then A4: dom (canFS S) = Seg (card S) by FINSEQ_1:def 3;
len (canFS (support b)) = card (support b) by FINSEQ_1:93;
then A5: dom (canFS (support b)) = Seg (card (support b)) by FINSEQ_1:def 3;
consider g being FinSequence of REAL such that
A6: Sum b = Sum g and
A7: g = b * (canFS (support b)) by Def2;
A8: dom b = A by PARTFUN1:def 2;
then A9: dom g = Seg (card (support b)) by A1, A7, A5, A3, RELAT_1:27, XBOOLE_1:1;
then A10: len g = card (support b) by FINSEQ_1:def 3;
A11: rng (canFS S) = S by FUNCT_2:def 3;
then A12: dom (b * (canFS S)) = Seg (card S) by A4, A8, RELAT_1:27;
then reconsider f = b * (canFS S) as FinSequence by FINSEQ_1:def 2;
rng f c= rng b by RELAT_1:26;
then rng f c= REAL by XBOOLE_1:1;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
take f ; :: thesis:
thus f = b * (canFS S) ; :: thesis:

per cases by A2, XXREAL_0:1;

suppose A13: card (support b) < card S ; :: thesis:

set dd = { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } ;

A14: now :: thesis:

consider x being object such that
A15: ( ( x in support b & not x in S ) or ( x in S & not x in support b ) ) by A13, TARSKI:2;
consider j being object such that
A16: j in dom (canFS S) and
A17: (canFS S) . j = x by A1, A11, A15, FUNCT_1:def 3;
reconsider j = j as Element of NAT by A16;
f . j = b . x by A16, A17, FUNCT_1:13;
then f . j = 0 by A1, A15, PRE_POLY:def 7;
then j in { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } by A4, A12, A16;
hence not { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } is empty ; :: thesis:

end;

reconsider gr = g as FinSequence of REAL ;
A18: { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } c= dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } ; :: thesis:
then ex j being Element of NAT st
( x = j & j in dom f & f . j = 0 ) ;
hence x in dom f ; :: thesis:

end;

then reconsider dd = { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } as non empty finite set by A14;
consider d being Element of NAT such that
A19: card S = (card (support b)) + d and
1 <= d by A13, FINSEQ_4:84;
set h = d |-> (In (0,REAL));
set F = gr ^ (d |-> (In (0,REAL)));
( rng (canFS dd) = dd & dd c= NAT ) by A18, FUNCT_2:def 3, XBOOLE_1:1;
then reconsider cdd = canFS dd as FinSequence of NAT by FINSEQ_1:def 4;
set cdi = cdd " ;
reconsider cdi = cdd " as Function of dd,(Seg (card dd)) by FINSEQ_1:95;
reconsider cdi = cdi as Function of dd,NAT by FUNCT_2:7;
deffunc H₁( object ) -> Element of NAT = (cdi /. $1) + (card (support b));
consider z being Function such that
A20: dom z = dd and
A21: for x being object st x in dd holds
z . x = H₁(x) from FUNCT_1:sch 3();
set p = (((canFS (support b)) ") * (canFS S)) +* z;
A22: dom cdi = dd by FUNCT_2:def 1;
set cSr = (canFS S) | ((dom f) \ dd);

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng ((canFS S) | ((dom f) \ dd)) ; :: thesis:
then consider x being object such that
A23: x in dom ((canFS S) | ((dom f) \ dd)) and
A24: y = ((canFS S) | ((dom f) \ dd)) . x by FUNCT_1:def 3;
A25: ((canFS S) | ((dom f) \ dd)) . x = (canFS S) . x by A23, FUNCT_1:47;
x in dom (canFS S) by A23, RELAT_1:57;
then reconsider j = x as Element of NAT ;
dom ((canFS S) | ((dom f) \ dd)) c= (dom f) \ dd by RELAT_1:58;
then A26: x in (findom f) \ dd by A23;
then not j in dd by XBOOLE_0:def 5;
then A27: f . j <> 0 by A26;
x in dom (canFS S) by A23, RELAT_1:57;
then b . ((canFS S) . j) <> 0 by A27, FUNCT_1:13;
hence y in support b by A24, A25, PRE_POLY:def 7; :: thesis:

end;

assume A28: y in support b ; :: thesis:
then consider x being object such that
A29: x in dom (canFS S) and
A30: y = (canFS S) . x by A1, A11, FUNCT_1:def 3;

now :: thesis:

assume x in dd ; :: thesis:
then consider j being Element of NAT such that
A31: j = x and
A32: ( j in dom f & f . j = 0 ) ;
0 = b . ((canFS S) . j) by A4, A12, A32, FUNCT_1:13;
hence contradiction by A28, A30, A31, PRE_POLY:def 7; :: thesis:

end;

then x in (dom f) \ dd by A4, A12, A29, XBOOLE_0:def 5;
hence y in rng ((canFS S) | ((dom f) \ dd)) by A29, A30, FUNCT_1:50; :: thesis:

end;

then A33: rng ((canFS S) | ((dom f) \ dd)) = support b by TARSKI:2;
((findom f) \ dd) /\ (dom f) = (dom f) \ dd by XBOOLE_1:28;
then ( (canFS S) | ((dom f) \ dd) is one-to-one & dom ((canFS S) | ((dom f) \ dd)) = (dom f) \ dd ) by A4, A12, FUNCT_1:52, RELAT_1:61;
then support b,(dom f) \ dd are_equipotent by A33, WELLORD2:def 4;
then A34: card (support b) = card ((dom f) \ dd) by CARD_1:5;
card ((dom f) \ dd) = (card (dom f)) - (card dd) by A18, CARD_2:44;
then A35: (card (support b)) + (card dd) = card S by A12, A34, FINSEQ_1:57;

A36: now :: thesis:

A37: dom ((canFS (support b)) ") = support b by A3, FUNCT_1:33;
assume (dom (((canFS (support b)) ") * (canFS S))) /\ (dom z) <> {} ; :: thesis:
then consider x being object such that
A38: x in (dom (((canFS (support b)) ") * (canFS S))) /\ (dom z) by XBOOLE_0:def 1;
x in dom z by A38, XBOOLE_0:def 4;
then consider j being Element of NAT such that
A39: j = x and
j in dom f and
A40: f . j = 0 by A20;
A41: x in dom (((canFS (support b)) ") * (canFS S)) by A38, XBOOLE_0:def 4;
then j in dom (canFS S) by A39, FUNCT_1:11;
then f . j = b . ((canFS S) . j) by FUNCT_1:13;
then not (canFS S) . j in support b by A40, PRE_POLY:def 7;
hence contradiction by A41, A39, A37, FUNCT_1:11; :: thesis:

end;

len (gr ^ (d |-> (In (0,REAL)))) = (len g) + (len (d |-> (In (0,REAL)))) by FINSEQ_1:22
.= card S by A10, A19, CARD_1:def 7 ;
then A42: dom (gr ^ (d |-> (In (0,REAL)))) = Seg (card S) by FINSEQ_1:def 3;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume A43: x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) ; :: thesis:

per cases by A43, XBOOLE_0:def 3;

suppose x in dom (((canFS (support b)) ") * (canFS S)) ; :: thesis:

hence x in dom (gr ^ (d |-> (In (0,REAL)))) by A4, A42, FUNCT_1:11; :: thesis:

end;

suppose x in dom z ; :: thesis:

hence x in dom (gr ^ (d |-> (In (0,REAL)))) by A12, A42, A18, A20; :: thesis:

end;

assume A44: x in dom (gr ^ (d |-> (In (0,REAL)))) ; :: thesis:
then reconsider i = x as Element of NAT ;

per cases ;

suppose f . x = 0 ; :: thesis:

then i in dom z by A12, A42, A20, A44;
hence x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) by XBOOLE_0:def 3; :: thesis:

end;

suppose A45: f . x <> 0 ; :: thesis:

f . i = b . ((canFS S) . i) by A4, A42, A44, FUNCT_1:13;
then (canFS S) . i in support b by A45, PRE_POLY:def 7;
then (canFS S) . i in dom ((canFS (support b)) ") by A3, FUNCT_1:33;
then i in dom (((canFS (support b)) ") * (canFS S)) by A4, A42, A44, FUNCT_1:11;
hence x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) by XBOOLE_0:def 3; :: thesis:

end;

then A46: (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) = dom (gr ^ (d |-> (In (0,REAL)))) by TARSKI:2;
then A47: dom ((((canFS (support b)) ") * (canFS S)) +* z) = dom (gr ^ (d |-> (In (0,REAL)))) by FUNCT_4:def 1;
len cdd = card dd by FINSEQ_1:93;
then A48: dom cdd = Seg d by A19, A35, FINSEQ_1:def 3;
then A49: rng cdi = Seg d by FUNCT_1:33;
A50: rng z c= Seg (card S)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng z ; :: thesis:
then consider x being object such that
A51: x in dom z and
A52: y = z . x by FUNCT_1:def 3;
A53: ( cdi /. x = cdi . x & cdi . x in Seg d ) by A22, A49, A20, A51, FUNCT_1:3, PARTFUN1:def 6;
then 1 <= cdi /. x by FINSEQ_1:1;
then A54: 1 <= (cdi /. x) + (card (support b)) by NAT_1:12;
cdi /. x <= d by A53, FINSEQ_1:1;
then A55: (cdi /. x) + (card (support b)) <= d + (card (support b)) by XREAL_1:6;
y = (cdi /. x) + (card (support b)) by A20, A21, A51, A52;
hence y in Seg (card S) by A19, A54, A55, FINSEQ_1:1; :: thesis:

end;

A56: now :: thesis:

let x be object ; :: thesis:
assume A57: x in dom (gr ^ (d |-> (In (0,REAL)))) ; :: thesis:

per cases by A46, A57, XBOOLE_0:def 3;

suppose A58: x in dom (((canFS (support b)) ") * (canFS S)) ; :: thesis:

end;

suppose x in dom z ; :: thesis:

then ( ((((canFS (support b)) ") * (canFS S)) +* z) . x = z . x & z . x in rng z ) by FUNCT_1:3, FUNCT_4:13;
hence ((((canFS (support b)) ") * (canFS S)) +* z) . x in dom (gr ^ (d |-> (In (0,REAL)))) by A42, A50; :: thesis:

end;

A61: dom ((((canFS (support b)) ") * (canFS S)) +* z) = (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) by FUNCT_4:def 1;
reconsider p = (((canFS (support b)) ") * (canFS S)) +* z as Function of (dom (gr ^ (d |-> (In (0,REAL))))),(dom (gr ^ (d |-> (In (0,REAL))))) by A47, A56, FUNCT_2:3;
len (d |-> (In (0,REAL))) = d by CARD_1:def 7;
then A62: dom (d |-> (In (0,REAL))) = Seg d by FINSEQ_1:def 3;
A63: rng cdd = dd by FUNCT_2:def 3;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in rng p ; :: thesis:
then consider a being object such that
A64: a in dom p and
A65: x = p . a by FUNCT_1:def 3;

per cases by A64, FUNCT_4:12;

suppose A66: a in dom (((canFS (support b)) ") * (canFS S)) ; :: thesis:

end;

suppose a in dom z ; :: thesis:

then ( z . a in rng z & p . a = z . a ) by FUNCT_1:3, FUNCT_4:13;
hence x in dom (gr ^ (d |-> (In (0,REAL)))) by A42, A50, A65; :: thesis:

end;

assume A69: x in dom (gr ^ (d |-> (In (0,REAL)))) ; :: thesis:
then reconsider j = x as Element of NAT ;

per cases by A69, FINSEQ_1:25;

suppose A70: j in dom gr ; :: thesis:

then A71: (canFS (support b)) . j in support b by A5, A3, A9, FUNCT_1:3;
then A72: ((canFS S) ") . ((canFS (support b)) . j) in Seg (card S) by A1, A4, A11, FUNCT_1:32;

now :: thesis:

assume ((canFS S) ") . ((canFS (support b)) . j) in dom z ; :: thesis:
then A73: ex k being Element of NAT st
( k = ((canFS S) ") . ((canFS (support b)) . j) & k in dom f & f . k = 0 ) by A20;
(b * (canFS S)) . (((canFS S) ") . ((canFS (support b)) . j)) = b . ((canFS S) . (((canFS S) ") . ((canFS (support b)) . j))) by A4, A72, FUNCT_1:13
.= b . ((canFS (support b)) . j) by A1, A11, A71, FUNCT_1:35 ;
hence contradiction by A71, A73, PRE_POLY:def 7; :: thesis:

end;

then p . (((canFS S) ") . ((canFS (support b)) . j)) = (((canFS (support b)) ") * (canFS S)) . (((canFS S) ") . ((canFS (support b)) . j)) by FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . (((canFS S) ") . ((canFS (support b)) . j))) by A4, A72, FUNCT_1:13
.= ((canFS (support b)) ") . ((canFS (support b)) . j) by A1, A11, A71, FUNCT_1:35
.= j by A5, A9, A70, FUNCT_1:34 ;
hence x in rng p by A42, A47, A72, FUNCT_1:3; :: thesis:

end;

suppose ex n being Nat st
( n in dom (d |-> (In (0,REAL))) & j = (len gr) + n ) ; :: thesis:

then consider n being Nat such that
A74: n in dom (d |-> (In (0,REAL))) and
A75: j = (len gr) + n ;
A76: cdd . n in dd by A62, A48, A63, A74, FUNCT_1:3;
p . (cdd . n) = z . (cdd . n) by A62, A48, A63, A20, A74, FUNCT_1:3, FUNCT_4:13
.= (cdi /. (cdd . n)) + (card (support b)) by A62, A48, A63, A21, A74, FUNCT_1:3
.= (cdi . (cdd . n)) + (card (support b)) by A62, A48, A63, A22, A74, FUNCT_1:3, PARTFUN1:def 6
.= n + (card (support b)) by A62, A48, A74, FUNCT_1:34
.= j by A9, A75, FINSEQ_1:def 3 ;
hence x in rng p by A12, A42, A18, A47, A76, FUNCT_1:3; :: thesis:

end;

then A77: rng p = dom (gr ^ (d |-> (In (0,REAL)))) by TARSKI:2;
then A78: dom ((gr ^ (d |-> (In (0,REAL)))) * p) = dom (gr ^ (d |-> (In (0,REAL)))) by A47, RELAT_1:27;

now :: thesis:

let x be object ; :: thesis:
assume A79: x in dom f ; :: thesis:

per cases ;

suppose A80: f . x = 0 ; :: thesis:

reconsider cdix = cdi /. x as Element of NAT ;
reconsider px = p . x as Element of NAT by ORDINAL1:def 12;
reconsider j = x as Element of NAT by A79;
A81: j in dom z by A20, A79, A80;
then A82: p . x = z . x by FUNCT_4:13
.= (cdi /. x) + (card (support b)) by A20, A21, A81 ;
A83: cdi . x in Seg (card dd) by A20, A81, FUNCT_2:5;
dom cdi = dd by FUNCT_2:def 1;
then A84: cdi /. x = cdi . x by A20, A81, PARTFUN1:def 6;
thus f . x = (d |-> (In (0,REAL))) . cdix by A80
.= (gr ^ (d |-> (In (0,REAL)))) . px by A10, A19, A62, A35, A82, A84, A83, FINSEQ_1:def 7
.= ((gr ^ (d |-> (In (0,REAL)))) * p) . x by A12, A42, A78, A79, FUNCT_1:12 ; :: thesis:

end;

suppose A85: f . x <> 0 ; :: thesis:

reconsider px = p . x as Element of NAT by ORDINAL1:def 12;
f . x = b . ((canFS S) . x) by A79, FUNCT_1:12;
then (canFS S) . x in support b by A85, PRE_POLY:def 7;
then A86: (canFS S) . x in rng (canFS (support b)) by FUNCT_2:def 3;
then A87: ((canFS (support b)) ") . ((canFS S) . x) in dom (canFS (support b)) by FUNCT_1:32;

now :: thesis:

assume x in dd ; :: thesis:
then ex j being Element of NAT st
( j = x & j in dom f & f . j = 0 ) ;
hence contradiction by A85; :: thesis:

end;

then A88: p . x = (((canFS (support b)) ") * (canFS S)) . x by A20, FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . x) by A4, A12, A79, FUNCT_1:13 ;
thus f . x = b . ((canFS S) . x) by A79, FUNCT_1:12
.= b . ((canFS (support b)) . px) by A86, A88, FUNCT_1:32
.= g . px by A7, A87, A88, FUNCT_1:13
.= (gr ^ (d |-> (In (0,REAL)))) . px by A5, A9, A87, A88, FINSEQ_1:def 7
.= ((gr ^ (d |-> (In (0,REAL)))) * p) . x by A12, A42, A78, A79, FUNCT_1:12 ; :: thesis:

end;

then A89: f = (gr ^ (d |-> (In (0,REAL)))) * p by A4, A11, A8, A42, A78, RELAT_1:27;
A90: p is one-to-one

proof

let a, c be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A91: ( a in dom p & c in dom p ) and
A92: p . a = p . c ; :: thesis:

per cases by A61, A91, XBOOLE_0:def 3;

suppose A93: ( a in dom (((canFS (support b)) ") * (canFS S)) & c in dom (((canFS (support b)) ") * (canFS S)) ) ; :: thesis:

then (canFS S) . a in dom ((canFS (support b)) ") by FUNCT_1:11;
then (canFS S) . a in rng (canFS (support b)) by FUNCT_1:33;
then A94: (canFS (support b)) . (((canFS (support b)) ") . ((canFS S) . a)) = (canFS S) . a by FUNCT_1:35;
a in dom (canFS S) by A93, FUNCT_1:11;
then A95: ((canFS S) ") . ((canFS S) . a) = a by FUNCT_1:34;
(canFS S) . c in dom ((canFS (support b)) ") by A93, FUNCT_1:11;
then A96: (canFS S) . c in rng (canFS (support b)) by FUNCT_1:33;
not c in dom z by A36, A93, XBOOLE_0:def 4;
then A97: p . c = (((canFS (support b)) ") * (canFS S)) . c by FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . c) by A93, FUNCT_1:12 ;
A98: c in dom (canFS S) by A93, FUNCT_1:11;
not a in dom z by A36, A93, XBOOLE_0:def 4;
then p . a = (((canFS (support b)) ") * (canFS S)) . a by FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . a) by A93, FUNCT_1:12 ;
then ((canFS S) ") . ((canFS S) . a) = ((canFS S) ") . ((canFS S) . c) by A92, A97, A94, A96, FUNCT_1:35;
hence a = c by A95, A98, FUNCT_1:34; :: thesis:

end;

suppose A99: ( a in dom (((canFS (support b)) ") * (canFS S)) & c in dom z ) ; :: thesis:

then (canFS S) . a in dom ((canFS (support b)) ") by FUNCT_1:11;
then ((canFS (support b)) ") . ((canFS S) . a) in rng ((canFS (support b)) ") by FUNCT_1:3;
then A100: ((canFS (support b)) ") . ((canFS S) . a) in dom (canFS (support b)) by FUNCT_1:33;
not a in dom z by A36, A99, XBOOLE_0:def 4;
then A101: p . a = (((canFS (support b)) ") * (canFS S)) . a by FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . a) by A99, FUNCT_1:12 ;
p . c = z . c by A99, FUNCT_4:13
.= (cdi /. c) + (card (support b)) by A20, A21, A99 ;
then (cdi /. c) + (card (support b)) <= 0 + (card (support b)) by A5, A92, A101, A100, FINSEQ_1:1;
then cdi /. c = 0 by XREAL_1:6;
then A102: cdi . c = 0 by A22, A20, A99, PARTFUN1:def 6;
cdi . c in rng cdi by A22, A20, A99, FUNCT_1:3;
hence a = c by A49, A102, FINSEQ_1:1; :: thesis:

end;

suppose A103: ( a in dom z & c in dom (((canFS (support b)) ") * (canFS S)) ) ; :: thesis:

then (canFS S) . c in dom ((canFS (support b)) ") by FUNCT_1:11;
then ((canFS (support b)) ") . ((canFS S) . c) in rng ((canFS (support b)) ") by FUNCT_1:3;
then A104: ((canFS (support b)) ") . ((canFS S) . c) in dom (canFS (support b)) by FUNCT_1:33;
not c in dom z by A36, A103, XBOOLE_0:def 4;
then A105: p . c = (((canFS (support b)) ") * (canFS S)) . c by FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . c) by A103, FUNCT_1:12 ;
p . a = z . a by A103, FUNCT_4:13
.= (cdi /. a) + (card (support b)) by A20, A21, A103 ;
then (cdi /. a) + (card (support b)) <= 0 + (card (support b)) by A5, A92, A105, A104, FINSEQ_1:1;
then cdi /. a = 0 by XREAL_1:6;
then A106: cdi . a = 0 by A22, A20, A103, PARTFUN1:def 6;
cdi . a in rng cdi by A22, A20, A103, FUNCT_1:3;
hence a = c by A49, A106, FINSEQ_1:1; :: thesis:

end;

suppose A107: ( a in dom z & c in dom z ) ; :: thesis:

then A108: ( cdi /. a = cdi . a & cdi /. c = cdi . c ) by A22, A20, PARTFUN1:def 6;
A109: p . c = z . c by A107, FUNCT_4:13
.= (cdi /. c) + (card (support b)) by A20, A21, A107 ;
p . a = z . a by A107, FUNCT_4:13
.= (cdi /. a) + (card (support b)) by A20, A21, A107 ;
hence a = c by A22, A20, A92, A107, A109, A108, FUNCT_1:def 4; :: thesis:

end;

Sum (d |-> (In (0,REAL))) = 0 by RVSUM_1:81;
then A110: Sum gr = (Sum gr) + (Sum (d |-> (In (0,REAL))))
.= Sum (gr ^ (d |-> (In (0,REAL)))) by RVSUM_1:75 ;
p is onto by A77, FUNCT_2:def 3;
hence Sum b = Sum f by A6, A90, A89, A110, FINSOP_1:7; :: thesis:

end;

suppose card (support b) = card S ; :: thesis:

hence Sum b = Sum f by A1, A6, A7, CARD_2:102; :: thesis:

end;