let A be set ; :: thesis: for S being finite Subset of A
for b being Rbag of A st support b c= S holds
ex f being FinSequence of REAL st
( f = b * () & Sum b = Sum f )

let S be finite Subset of A; :: thesis: for b being Rbag of A st support b c= S holds
ex f being FinSequence of REAL st
( f = b * () & Sum b = Sum f )

let b be Rbag of A; :: thesis: ( support b c= S implies ex f being FinSequence of REAL st
( f = b * () & Sum b = Sum f ) )

assume A1: support b c= S ; :: thesis: ex f being FinSequence of REAL st
( f = b * () & Sum b = Sum f )

A2: card () <= card S by ;
set cs = canFS ();
A3: rng (canFS ()) = support b by FUNCT_2:def 3;
set cS = canFS S;
set f = b * ();
len () = card S by FINSEQ_1:93;
then A4: dom () = Seg (card S) by FINSEQ_1:def 3;
len (canFS ()) = card () by FINSEQ_1:93;
then A5: dom (canFS ()) = Seg (card ()) by FINSEQ_1:def 3;
consider g being FinSequence of REAL such that
A6: Sum b = Sum g and
A7: g = b * (canFS ()) by Def2;
A8: dom b = A by PARTFUN1:def 2;
then A9: dom g = Seg (card ()) by ;
then A10: len g = card () by FINSEQ_1:def 3;
A11: rng () = S by FUNCT_2:def 3;
then A12: dom (b * ()) = Seg (card S) by ;
then reconsider f = b * () 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: ( f = b * () & Sum b = Sum f )
thus f = b * () ; :: thesis: Sum b = Sum f
per cases ( card () < card S or card () = card S ) by ;
suppose A13: card () < card S ; :: thesis: Sum b = Sum f
set dd = { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } ;
A14: now :: thesis: not { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } is empty
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 ;
consider j being object such that
A16: j in dom () and
A17: (canFS S) . j = x by ;
reconsider j = j as Element of NAT by A16;
f . j = b . x by ;
then f . j = 0 by ;
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: verum
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: ( not x in { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } or x in dom f )
assume x in { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } ; :: thesis: x in dom f
then ex j being Element of NAT st
( x = j & j in dom f & f . j = 0 ) ;
hence x in dom f ; :: thesis: verum
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 ()) + d and
1 <= d by ;
set h = d |-> (In (0,REAL));
set F = gr ^ (d |-> (In (0,REAL)));
( rng (canFS dd) = dd & dd c= NAT ) by ;
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 H1( object ) -> Element of NAT = (cdi /. \$1) + (card ());
consider z being Function such that
A20: dom z = dd and
A21: for x being object st x in dd holds
z . x = H1(x) from set p = (((canFS ()) ") * ()) +* z;
A22: dom cdi = dd by FUNCT_2:def 1;
set cSr = () | ((dom f) \ dd);
now :: thesis: for y being object holds
( ( y in rng (() | ((dom f) \ dd)) implies y in support b ) & ( y in support b implies y in rng (() | ((dom f) \ dd)) ) )
let y be object ; :: thesis: ( ( y in rng (() | ((dom f) \ dd)) implies y in support b ) & ( y in support b implies y in rng (() | ((dom f) \ dd)) ) )
hereby :: thesis: ( y in support b implies y in rng (() | ((dom f) \ dd)) )
assume y in rng (() | ((dom f) \ dd)) ; :: thesis:
then consider x being object such that
A23: x in dom (() | ((dom f) \ dd)) and
A24: y = (() | ((dom f) \ dd)) . x by FUNCT_1:def 3;
A25: ((canFS S) | ((dom f) \ dd)) . x = () . x by ;
x in dom () by ;
then reconsider j = x as Element of NAT ;
dom (() | ((dom f) \ dd)) c= (dom f) \ dd by RELAT_1:58;
then A26: x in () \ dd by A23;
then not j in dd by XBOOLE_0:def 5;
then A27: f . j <> 0 by A26;
x in dom () by ;
then b . (() . j) <> 0 by ;
hence y in support b by ; :: thesis: verum
end;
assume A28: y in support b ; :: thesis: y in rng (() | ((dom f) \ dd))
then consider x being object such that
A29: x in dom () and
A30: y = () . x by ;
now :: thesis: not x in dd
assume x in dd ; :: thesis: contradiction
then consider j being Element of NAT such that
A31: j = x and
A32: ( j in dom f & f . j = 0 ) ;
0 = b . (() . j) by ;
hence contradiction by A28, A30, A31, PRE_POLY:def 7; :: thesis: verum
end;
then x in (dom f) \ dd by ;
hence y in rng (() | ((dom f) \ dd)) by ; :: thesis: verum
end;
then A33: rng (() | ((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 (() | ((dom f) \ dd)) = (dom f) \ dd ) by ;
then support b,(dom f) \ dd are_equipotent by ;
then A34: card () = card ((dom f) \ dd) by CARD_1:5;
card ((dom f) \ dd) = (card (dom f)) - (card dd) by ;
then A35: (card ()) + (card dd) = card S by ;
A36: now :: thesis: not (dom (((canFS ()) ") * ())) /\ (dom z) <> {}
A37: dom ((canFS ()) ") = support b by ;
assume (dom (((canFS ()) ") * ())) /\ (dom z) <> {} ; :: thesis: contradiction
then consider x being object such that
A38: x in (dom (((canFS ()) ") * ())) /\ (dom z) by XBOOLE_0:def 1;
x in dom z by ;
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 ()) ") * ()) by ;
then j in dom () by ;
then f . j = b . (() . j) by FUNCT_1:13;
then not (canFS S) . j in support b by ;
hence contradiction by A41, A39, A37, FUNCT_1:11; :: thesis: verum
end;
len (gr ^ (d |-> (In (0,REAL)))) = (len g) + (len (d |-> (In (0,REAL)))) by FINSEQ_1:22
.= card S by ;
then A42: dom (gr ^ (d |-> (In (0,REAL)))) = Seg (card S) by FINSEQ_1:def 3;
now :: thesis: for x being object holds
( ( x in (dom (((canFS ()) ") * ())) \/ (dom z) implies x in dom (gr ^ (d |-> (In (0,REAL)))) ) & ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies x in (dom (((canFS ()) ") * ())) \/ (dom z) ) )
let x be object ; :: thesis: ( ( x in (dom (((canFS ()) ") * ())) \/ (dom z) implies x in dom (gr ^ (d |-> (In (0,REAL)))) ) & ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies b1 in (dom (((canFS ()) ") * ())) \/ (dom z) ) )
hereby :: thesis: ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies b1 in (dom (((canFS ()) ") * ())) \/ (dom z) )
assume A43: x in (dom (((canFS ()) ") * ())) \/ (dom z) ; :: thesis: x in dom (gr ^ (d |-> (In (0,REAL))))
per cases ( x in dom (((canFS ()) ") * ()) or x in dom z ) by ;
suppose x in dom (((canFS ()) ") * ()) ; :: thesis: x in dom (gr ^ (d |-> (In (0,REAL))))
hence x in dom (gr ^ (d |-> (In (0,REAL)))) by ; :: thesis: verum
end;
suppose x in dom z ; :: thesis: x in dom (gr ^ (d |-> (In (0,REAL))))
hence x in dom (gr ^ (d |-> (In (0,REAL)))) by A12, A42, A18, A20; :: thesis: verum
end;
end;
end;
assume A44: x in dom (gr ^ (d |-> (In (0,REAL)))) ; :: thesis: b1 in (dom (((canFS ()) ") * ())) \/ (dom z)
then reconsider i = x as Element of NAT ;
per cases ( f . x = 0 or f . x <> 0 ) ;
suppose f . x = 0 ; :: thesis: b1 in (dom (((canFS ()) ") * ())) \/ (dom z)
then i in dom z by A12, A42, A20, A44;
hence x in (dom (((canFS ()) ") * ())) \/ (dom z) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose A45: f . x <> 0 ; :: thesis: b1 in (dom (((canFS ()) ") * ())) \/ (dom z)
f . i = b . (() . i) by ;
then (canFS S) . i in support b by ;
then (canFS S) . i in dom ((canFS ()) ") by ;
then i in dom (((canFS ()) ") * ()) by ;
hence x in (dom (((canFS ()) ") * ())) \/ (dom z) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then A46: (dom (((canFS ()) ") * ())) \/ (dom z) = dom (gr ^ (d |-> (In (0,REAL)))) by TARSKI:2;
then A47: dom ((((canFS ()) ") * ()) +* 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 ;
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: ( not y in rng z or y in Seg (card S) )
assume y in rng z ; :: thesis: y in Seg (card S)
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 ;
then 1 <= cdi /. x by FINSEQ_1:1;
then A54: 1 <= (cdi /. x) + (card ()) by NAT_1:12;
cdi /. x <= d by ;
then A55: (cdi /. x) + (card ()) <= d + (card ()) by XREAL_1:6;
y = (cdi /. x) + (card ()) by A20, A21, A51, A52;
hence y in Seg (card S) by ; :: thesis: verum
end;
A56: now :: thesis: for x being object st x in dom (gr ^ (d |-> (In (0,REAL)))) holds
((((canFS ()) ") * ()) +* z) . x in dom (gr ^ (d |-> (In (0,REAL))))
let x be object ; :: thesis: ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies ((((canFS ()) ") * ()) +* z) . b1 in dom (gr ^ (d |-> (In (0,REAL)))) )
assume A57: x in dom (gr ^ (d |-> (In (0,REAL)))) ; :: thesis: ((((canFS ()) ") * ()) +* z) . b1 in dom (gr ^ (d |-> (In (0,REAL))))
per cases ( x in dom (((canFS ()) ") * ()) or x in dom z ) by ;
suppose A58: x in dom (((canFS ()) ") * ()) ; :: thesis: ((((canFS ()) ") * ()) +* z) . b1 in dom (gr ^ (d |-> (In (0,REAL))))
then (((canFS ()) ") * ()) . x in rng (((canFS ()) ") * ()) by FUNCT_1:3;
then (((canFS ()) ") * ()) . x in rng ((canFS ()) ") by FUNCT_1:14;
then A59: (((canFS ()) ") * ()) . x in dom (canFS ()) by FUNCT_1:33;
not x in dom z by ;
then A60: ((((canFS ()) ") * ()) +* z) . x = (((canFS ()) ") * ()) . x by FUNCT_4:11;
Seg (card ()) c= Seg (card S) by ;
hence ((((canFS ()) ") * ()) +* z) . x in dom (gr ^ (d |-> (In (0,REAL)))) by A5, A42, A60, A59; :: thesis: verum
end;
suppose x in dom z ; :: thesis: ((((canFS ()) ") * ()) +* z) . b1 in dom (gr ^ (d |-> (In (0,REAL))))
then ( ((((canFS ()) ") * ()) +* z) . x = z . x & z . x in rng z ) by ;
hence ((((canFS ()) ") * ()) +* z) . x in dom (gr ^ (d |-> (In (0,REAL)))) by ; :: thesis: verum
end;
end;
end;
A61: dom ((((canFS ()) ") * ()) +* z) = (dom (((canFS ()) ") * ())) \/ (dom z) by FUNCT_4:def 1;
reconsider p = (((canFS ()) ") * ()) +* z as Function of (dom (gr ^ (d |-> (In (0,REAL))))),(dom (gr ^ (d |-> (In (0,REAL))))) by ;
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: for x being object holds
( ( x in rng p implies x in dom (gr ^ (d |-> (In (0,REAL)))) ) & ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies x in rng p ) )
let x be object ; :: thesis: ( ( x in rng p implies x in dom (gr ^ (d |-> (In (0,REAL)))) ) & ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies b1 in rng p ) )
hereby :: thesis: ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies b1 in rng p )
assume x in rng p ; :: thesis: x in dom (gr ^ (d |-> (In (0,REAL))))
then consider a being object such that
A64: a in dom p and
A65: x = p . a by FUNCT_1:def 3;
per cases ( a in dom (((canFS ()) ") * ()) or a in dom z ) by ;
suppose A66: a in dom (((canFS ()) ") * ()) ; :: thesis: x in dom (gr ^ (d |-> (In (0,REAL))))
then (canFS S) . a in dom ((canFS ()) ") by FUNCT_1:11;
then ((canFS ()) ") . (() . a) in rng ((canFS ()) ") by FUNCT_1:3;
then A67: ((canFS ()) ") . (() . a) in dom (canFS ()) by FUNCT_1:33;
not a in dom z by ;
then A68: p . a = (((canFS ()) ") * ()) . a by FUNCT_4:11
.= ((canFS ()) ") . (() . a) by ;
dom (canFS ()) c= dom (gr ^ (d |-> (In (0,REAL)))) by ;
hence x in dom (gr ^ (d |-> (In (0,REAL)))) by ; :: thesis: verum
end;
suppose a in dom z ; :: thesis: x in dom (gr ^ (d |-> (In (0,REAL))))
then ( z . a in rng z & p . a = z . a ) by ;
hence x in dom (gr ^ (d |-> (In (0,REAL)))) by ; :: thesis: verum
end;
end;
end;
assume A69: x in dom (gr ^ (d |-> (In (0,REAL)))) ; :: thesis: b1 in rng p
then reconsider j = x as Element of NAT ;
per cases ( j in dom gr or ex n being Nat st
( n in dom (d |-> (In (0,REAL))) & j = (len gr) + n ) )
by ;
suppose A70: j in dom gr ; :: thesis: b1 in rng p
then A71: (canFS ()) . j in support b by ;
then A72: ((canFS S) ") . ((canFS ()) . j) in Seg (card S) by ;
now :: thesis: not (() ") . ((canFS ()) . j) in dom z
assume ((canFS S) ") . ((canFS ()) . j) in dom z ; :: thesis: contradiction
then A73: ex k being Element of NAT st
( k = (() ") . ((canFS ()) . j) & k in dom f & f . k = 0 ) by A20;
(b * ()) . ((() ") . ((canFS ()) . j)) = b . (() . ((() ") . ((canFS ()) . j))) by
.= b . ((canFS ()) . j) by ;
hence contradiction by A71, A73, PRE_POLY:def 7; :: thesis: verum
end;
then p . ((() ") . ((canFS ()) . j)) = (((canFS ()) ") * ()) . ((() ") . ((canFS ()) . j)) by FUNCT_4:11
.= ((canFS ()) ") . (() . ((() ") . ((canFS ()) . j))) by
.= ((canFS ()) ") . ((canFS ()) . j) by
.= j by ;
hence x in rng p by ; :: thesis: verum
end;
suppose ex n being Nat st
( n in dom (d |-> (In (0,REAL))) & j = (len gr) + n ) ; :: thesis: b1 in rng p
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 ;
p . (cdd . n) = z . (cdd . n) by
.= (cdi /. (cdd . n)) + (card ()) by
.= (cdi . (cdd . n)) + (card ()) by
.= n + (card ()) by
.= j by ;
hence x in rng p by ; :: thesis: verum
end;
end;
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 ;
now :: thesis: for x being object st x in dom f holds
f . x = ((gr ^ (d |-> (In (0,REAL)))) * p) . x
let x be object ; :: thesis: ( x in dom f implies f . b1 = ((gr ^ (d |-> (In (0,REAL)))) * p) . b1 )
assume A79: x in dom f ; :: thesis: f . b1 = ((gr ^ (d |-> (In (0,REAL)))) * p) . b1
per cases ( f . x = 0 or f . x <> 0 ) ;
suppose A80: f . x = 0 ; :: thesis: f . b1 = ((gr ^ (d |-> (In (0,REAL)))) * p) . b1
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 ;
then A82: p . x = z . x by FUNCT_4:13
.= (cdi /. x) + (card ()) by ;
A83: cdi . x in Seg (card dd) by ;
dom cdi = dd by FUNCT_2:def 1;
then A84: cdi /. x = cdi . x by ;
thus f . x = (d |-> (In (0,REAL))) . cdix by A80
.= (gr ^ (d |-> (In (0,REAL)))) . px by
.= ((gr ^ (d |-> (In (0,REAL)))) * p) . x by ; :: thesis: verum
end;
suppose A85: f . x <> 0 ; :: thesis: f . b1 = ((gr ^ (d |-> (In (0,REAL)))) * p) . b1
reconsider px = p . x as Element of NAT by ORDINAL1:def 12;
f . x = b . (() . x) by ;
then (canFS S) . x in support b by ;
then A86: (canFS S) . x in rng (canFS ()) by FUNCT_2:def 3;
then A87: ((canFS ()) ") . (() . x) in dom (canFS ()) by FUNCT_1:32;
now :: thesis: not x in dd
assume x in dd ; :: thesis: contradiction
then ex j being Element of NAT st
( j = x & j in dom f & f . j = 0 ) ;
hence contradiction by A85; :: thesis: verum
end;
then A88: p . x = (((canFS ()) ") * ()) . x by
.= ((canFS ()) ") . (() . x) by ;
thus f . x = b . (() . x) by
.= b . ((canFS ()) . px) by
.= g . px by
.= (gr ^ (d |-> (In (0,REAL)))) . px by
.= ((gr ^ (d |-> (In (0,REAL)))) * p) . x by ; :: thesis: verum
end;
end;
end;
then A89: f = (gr ^ (d |-> (In (0,REAL)))) * p by ;
A90: p is one-to-one
proof
let a, c be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in proj1 p or not c in proj1 p or not p . a = p . c or a = c )
assume that
A91: ( a in dom p & c in dom p ) and
A92: p . a = p . c ; :: thesis: a = c
per cases ( ( a in dom (((canFS ()) ") * ()) & c in dom (((canFS ()) ") * ()) ) or ( a in dom (((canFS ()) ") * ()) & c in dom z ) or ( a in dom z & c in dom (((canFS ()) ") * ()) ) or ( a in dom z & c in dom z ) ) by ;
suppose A93: ( a in dom (((canFS ()) ") * ()) & c in dom (((canFS ()) ") * ()) ) ; :: thesis: a = c
then (canFS S) . a in dom ((canFS ()) ") by FUNCT_1:11;
then (canFS S) . a in rng (canFS ()) by FUNCT_1:33;
then A94: (canFS ()) . (((canFS ()) ") . (() . a)) = () . a by FUNCT_1:35;
a in dom () by ;
then A95: ((canFS S) ") . (() . a) = a by FUNCT_1:34;
(canFS S) . c in dom ((canFS ()) ") by ;
then A96: (canFS S) . c in rng (canFS ()) by FUNCT_1:33;
not c in dom z by ;
then A97: p . c = (((canFS ()) ") * ()) . c by FUNCT_4:11
.= ((canFS ()) ") . (() . c) by ;
A98: c in dom () by ;
not a in dom z by ;
then p . a = (((canFS ()) ") * ()) . a by FUNCT_4:11
.= ((canFS ()) ") . (() . a) by ;
then ((canFS S) ") . (() . a) = (() ") . (() . c) by ;
hence a = c by ; :: thesis: verum
end;
suppose A99: ( a in dom (((canFS ()) ") * ()) & c in dom z ) ; :: thesis: a = c
then (canFS S) . a in dom ((canFS ()) ") by FUNCT_1:11;
then ((canFS ()) ") . (() . a) in rng ((canFS ()) ") by FUNCT_1:3;
then A100: ((canFS ()) ") . (() . a) in dom (canFS ()) by FUNCT_1:33;
not a in dom z by ;
then A101: p . a = (((canFS ()) ") * ()) . a by FUNCT_4:11
.= ((canFS ()) ") . (() . a) by ;
p . c = z . c by
.= (cdi /. c) + (card ()) by ;
then (cdi /. c) + (card ()) <= 0 + (card ()) by ;
then cdi /. c = 0 by XREAL_1:6;
then A102: cdi . c = 0 by ;
cdi . c in rng cdi by ;
hence a = c by ; :: thesis: verum
end;
suppose A103: ( a in dom z & c in dom (((canFS ()) ") * ()) ) ; :: thesis: a = c
then (canFS S) . c in dom ((canFS ()) ") by FUNCT_1:11;
then ((canFS ()) ") . (() . c) in rng ((canFS ()) ") by FUNCT_1:3;
then A104: ((canFS ()) ") . (() . c) in dom (canFS ()) by FUNCT_1:33;
not c in dom z by ;
then A105: p . c = (((canFS ()) ") * ()) . c by FUNCT_4:11
.= ((canFS ()) ") . (() . c) by ;
p . a = z . a by
.= (cdi /. a) + (card ()) by ;
then (cdi /. a) + (card ()) <= 0 + (card ()) by ;
then cdi /. a = 0 by XREAL_1:6;
then A106: cdi . a = 0 by ;
cdi . a in rng cdi by ;
hence a = c by ; :: thesis: verum
end;
suppose A107: ( a in dom z & c in dom z ) ; :: thesis: a = c
then A108: ( cdi /. a = cdi . a & cdi /. c = cdi . c ) by ;
A109: p . c = z . c by
.= (cdi /. c) + (card ()) by ;
p . a = z . a by
.= (cdi /. a) + (card ()) by ;
hence a = c by ; :: thesis: verum
end;
end;
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 ;
hence Sum b = Sum f by ; :: thesis: verum
end;
suppose card () = card S ; :: thesis: Sum b = Sum f
hence Sum b = Sum f by ; :: thesis: verum
end;
end;