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

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;

end;

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 ) } ;

A18: { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } c= dom f

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_{1}( 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_{1}(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);

((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;

.= 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;

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)

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;

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

A90: p is one-to-one

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;A14: now :: thesis: not { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } is empty

reconsider gr = g as FinSequence of REAL ;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;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

A18: { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } c= dom f

proof

then reconsider dd = { j where j is Element of NAT : ( j in dom f & f . j = 0 ) } as non empty finite set by A14;
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;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

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

consider z being Function such that

A20: dom z = dd and

A21: for x being object st x in dd holds

z . x = H

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)) ) )

then A33:
rng ((canFS S) | ((dom f) \ dd)) = support b
by TARSKI:2;( ( 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)) ) )

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;

hence y in rng ((canFS S) | ((dom f) \ dd)) by A29, A30, FUNCT_1:50; :: thesis: verum

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

assume A28:
y in support b
; :: thesis: 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;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

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

then
x in (dom f) \ dd
by A4, A12, A29, XBOOLE_0:def 5;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 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

hence y in rng ((canFS S) | ((dom f) \ dd)) by A29, A30, FUNCT_1:50; :: thesis: verum

((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) <> {}

len (gr ^ (d |-> (In (0,REAL)))) =
(len g) + (len (d |-> (In (0,REAL))))
by FINSEQ_1:22
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;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

.= 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) ) )

then A46:
(dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) = dom (gr ^ (d |-> (In (0,REAL))))
by TARSKI:2;( ( 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_{1} in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) ) )

_{1} in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z)

then reconsider i = x as Element of NAT ;

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

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

end;then reconsider i = x as Element of NAT ;

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

end;

suppose
f . x = 0
; :: thesis: b_{1} 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;hence x in (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z) by XBOOLE_0:def 3; :: thesis: verum

suppose A45:
f . x <> 0
; :: thesis: b_{1} 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;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

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;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

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))))

A61:
dom ((((canFS (support b)) ") * (canFS S)) +* z) = (dom (((canFS (support b)) ") * (canFS S))) \/ (dom z)
by FUNCT_4:def 1;((((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_{1} 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_{1} in dom (gr ^ (d |-> (In (0,REAL))))

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

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

end;

suppose A58:
x in dom (((canFS (support b)) ") * (canFS S))
; :: thesis: ((((canFS (support b)) ") * (canFS S)) +* z) . b_{1} 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;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

suppose
x in dom z
; :: thesis: ((((canFS (support b)) ") * (canFS S)) +* z) . b_{1} 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;hence ((((canFS (support b)) ") * (canFS S)) +* z) . x in dom (gr ^ (d |-> (In (0,REAL)))) by A42, A50; :: thesis: verum

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 ) )

then A77:
rng p = dom (gr ^ (d |-> (In (0,REAL))))
by TARSKI:2;( ( 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_{1} in rng p ) )

_{1} in rng p

then reconsider j = x as Element of NAT ;

end;hereby :: thesis: ( x in dom (gr ^ (d |-> (In (0,REAL)))) implies b_{1} in rng p )

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

end;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;

end;

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;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

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;

end;

( n in dom (d |-> (In (0,REAL))) & j = (len gr) + n ) ) by A69, FINSEQ_1:25;

suppose A70:
j in dom gr
; :: thesis: b_{1} 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;

.= ((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;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

then p . (((canFS S) ") . ((canFS (support b)) . j)) =
(((canFS (support b)) ") * (canFS S)) . (((canFS S) ") . ((canFS (support b)) . j))
by FUNCT_4:11
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 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

.= ((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

suppose
ex n being Nat st

( n in dom (d |-> (In (0,REAL))) & j = (len gr) + n ) ; :: thesis: b_{1} in rng p

( n in dom (d |-> (In (0,REAL))) & j = (len gr) + n ) ; :: thesis: b

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;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

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

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

let x be object ; :: thesis: ( x in dom f implies f . b_{1} = ((gr ^ (d |-> (In (0,REAL)))) * p) . b_{1} )

assume A79: x in dom f ; :: thesis: f . b_{1} = ((gr ^ (d |-> (In (0,REAL)))) * p) . b_{1}

end;assume A79: x in dom f ; :: thesis: f . b

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

end;

suppose A80:
f . x = 0
; :: thesis: f . b_{1} = ((gr ^ (d |-> (In (0,REAL)))) * p) . b_{1}

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;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

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

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;

.= ((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;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

then A88: p . x =
(((canFS (support b)) ") * (canFS S)) . x
by A20, FUNCT_4:11
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 ex j being Element of NAT st

( j = x & j in dom f & f . j = 0 ) ;

hence contradiction by A85; :: thesis: verum

.= ((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

A90: p is one-to-one

proof

Sum (d |-> (In (0,REAL))) = 0
by RVSUM_1:81;
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

end;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;

end;

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;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

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;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

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;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

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;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

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