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 * (canFS S) & 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 * (canFS S) & 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 * (canFS S) & Sum b = Sum f ) )
assume A1: support b c= S ; :: thesis: ex f being FinSequence of REAL st
( f = b * (canFS S) & Sum b = Sum f )
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: ( f = b * (canFS S) & Sum b = Sum f )
thus f = b * (canFS S) ; :: thesis: Sum b = Sum f

per cases ( card (support b) < card S or card (support b) = card S ) by A2, XXREAL_0:1;

suppose A13: card (support b) < 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 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: 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 (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: for y being object holds
( ( y in rng ((canFS S) | ((dom f) \ dd)) implies y in support b ) & ( y in support b implies y in rng ((canFS S) | ((dom f) \ dd)) ) )

let y be object ; :: thesis: ( ( y in rng ((canFS S) | ((dom f) \ dd)) implies y in support b ) & ( y in support b implies y in rng ((canFS S) | ((dom f) \ dd)) ) )

hereby :: thesis: ( y in support b implies y in rng ((canFS S) | ((dom f) \ dd)) )

assume y in rng ((canFS S) | ((dom f) \ dd)) ; :: thesis: y in support b
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: verum

end;

assume A28: y in support b ; :: thesis: y in rng ((canFS S) | ((dom f) \ dd))
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: 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 . ((canFS S) . j) by A4, A12, A32, FUNCT_1:13;
hence contradiction by A28, A30, A31, PRE_POLY:def 7; :: thesis: verum

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: verum

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: not (dom (((canFS (support b)) ") * (canFS S))) /\ (dom z) <> {}

A37: dom ((canFS (support b)) ") = support b by A3, FUNCT_1:33;
assume (dom (((canFS (support b)) ") * (canFS S))) /\ (dom z) <> {} ; :: thesis: contradiction
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: verum

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: for x being object holds
( ( x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) implies x in dom (gr ^ (d |-> (In (0,REAL)))) ) & ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) ) )

let x be object ; :: thesis: ( ( x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) implies x in dom (gr ^ (d |-> (In (0,REAL)))) ) & ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies b₁ in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) ) )

hereby :: thesis: ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies b₁ in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) )

assume A43: x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) ; :: thesis: x in dom (gr ^ (d |-> (In (0,REAL))))

per cases ( x in dom (((canFS (support b)) ") * (canFS S)) or x in dom z ) by A43, XBOOLE_0:def 3;

suppose x in dom (((canFS (support b)) ") * (canFS S)) ; :: thesis: x in dom (gr ^ (d |-> (In (0,REAL))))

hence x in dom (gr ^ (d |-> (In (0,REAL)))) by A4, A42, FUNCT_1:11; :: 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: b₁ in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z)
then reconsider i = x as Element of NAT ;

per cases ( f . x = 0 or f . x <> 0 ) ;

suppose f . x = 0 ; :: thesis: b₁ in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z)

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: verum

end;

suppose A45: f . x <> 0 ; :: thesis: b₁ in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z)

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: verum

end;

end;

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: ( 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 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: verum

end;

A56: now :: thesis: for x being object st x in dom (gr ^ (d |-> (In (0,REAL)))) holds
((((canFS (support b)) ") * (canFS S)) +* z) . x in dom (gr ^ (d |-> (In (0,REAL))))

let x be object ; :: thesis: ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies ((((canFS (support b)) ") * (canFS S)) +* z) . b₁ in dom (gr ^ (d |-> (In (0,REAL)))) )
assume A57: x in dom (gr ^ (d |-> (In (0,REAL)))) ; :: thesis: ((((canFS (support b)) ") * (canFS S)) +* z) . b₁ in dom (gr ^ (d |-> (In (0,REAL))))

per cases ( x in dom (((canFS (support b)) ") * (canFS S)) or x in dom z ) by A46, A57, XBOOLE_0:def 3;

suppose A58: x in dom (((canFS (support b)) ") * (canFS S)) ; :: thesis: ((((canFS (support b)) ") * (canFS S)) +* z) . b₁ in dom (gr ^ (d |-> (In (0,REAL))))

then (((canFS (support b)) ") * (canFS S)) . x in rng (((canFS (support b)) ") * (canFS S)) by FUNCT_1:3;
then (((canFS (support b)) ") * (canFS S)) . x in rng ((canFS (support b)) ") by FUNCT_1:14;
then A59: (((canFS (support b)) ") * (canFS S)) . x in dom (canFS (support b)) by FUNCT_1:33;
not x in dom z by A36, A58, XBOOLE_0:def 4;
then A60: ((((canFS (support b)) ") * (canFS S)) +* z) . x = (((canFS (support b)) ") * (canFS S)) . x by FUNCT_4:11;
Seg (card (support b)) c= Seg (card S) by A2, FINSEQ_1:5;
hence ((((canFS (support b)) ") * (canFS S)) +* z) . x in dom (gr ^ (d |-> (In (0,REAL)))) by A5, A42, A60, A59; :: thesis: verum

end;

suppose x in dom z ; :: thesis: ((((canFS (support b)) ") * (canFS S)) +* z) . b₁ in dom (gr ^ (d |-> (In (0,REAL))))

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: verum

end;

end;

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: 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 b₁ in rng p ) )

hereby :: thesis: ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies b₁ 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 (support b)) ") * (canFS S)) or a in dom z ) by A64, FUNCT_4:12;

suppose A66: a in dom (((canFS (support b)) ") * (canFS S)) ; :: thesis: x in dom (gr ^ (d |-> (In (0,REAL))))

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 A67: ((canFS (support b)) ") . ((canFS S) . a) in dom (canFS (support b)) by FUNCT_1:33;
not a in dom z by A36, A66, XBOOLE_0:def 4;
then A68: p . a = (((canFS (support b)) ") * (canFS S)) . a by FUNCT_4:11
.= ((canFS (support b)) ") . ((canFS S) . a) by A66, FUNCT_1:12 ;
dom (canFS (support b)) c= dom (gr ^ (d |-> (In (0,REAL)))) by A5, A2, A42, FINSEQ_1:5;
hence x in dom (gr ^ (d |-> (In (0,REAL)))) by A65, A68, A67; :: 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 FUNCT_1:3, FUNCT_4:13;
hence x in dom (gr ^ (d |-> (In (0,REAL)))) by A42, A50, A65; :: thesis: verum

end;

end;

end;

assume A69: x in dom (gr ^ (d |-> (In (0,REAL)))) ; :: thesis: b₁ 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 A69, FINSEQ_1:25;

suppose A70: j in dom gr ; :: thesis: b₁ in rng p

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: not ((canFS S) ") . ((canFS (support b)) . j) in dom z

assume ((canFS S) ") . ((canFS (support b)) . j) in dom z ; :: thesis: contradiction
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: verum

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: verum

end;

suppose ex n being Nat st
( n in dom (d |-> (In (0,REAL))) & j = (len gr) + n ) ; :: thesis: b₁ 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 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: 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 A47, RELAT_1:27;

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 . b₁ = ((gr ^ (d |-> (In (0,REAL)))) * p) . b₁ )
assume A79: x in dom f ; :: thesis: f . b₁ = ((gr ^ (d |-> (In (0,REAL)))) * p) . b₁

per cases ( f . x = 0 or f . x <> 0 ) ;

suppose A80: f . x = 0 ; :: thesis: f . b₁ = ((gr ^ (d |-> (In (0,REAL)))) * p) . b₁

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: verum

end;

suppose A85: f . x <> 0 ; :: thesis: f . b₁ = ((gr ^ (d |-> (In (0,REAL)))) * p) . b₁

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: 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 (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: verum

end;

end;

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: ( 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 (support b)) ") * (canFS S)) & c in dom (((canFS (support b)) ") * (canFS S)) ) or ( a in dom (((canFS (support b)) ") * (canFS S)) & c in dom z ) or ( a in dom z & c in dom (((canFS (support b)) ") * (canFS S)) ) or ( a in dom z & c in dom z ) ) 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: a = c

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: verum

end;

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

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: verum

end;

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

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: 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 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: 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 A77, FUNCT_2:def 3;
hence Sum b = Sum f by A6, A90, A89, A110, FINSOP_1:7; :: thesis: verum

end;

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

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

end;

end;