let A be set ; :: thesis: for S being finite Subset of A
for b being Rbag of 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 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 ; :: 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 )
set cS = canFS S;
set f = b * (canFS S);
len (canFS S) = card S
by Def1;
then A2:
dom (canFS S) = Seg (card S)
by FINSEQ_1:def 3;
A3:
rng (canFS S) = S
by FUNCT_2:def 3;
A5:
dom b = A
by PARTFUN1:def 4;
then A6:
dom (b * (canFS S)) = Seg (card S)
by A2, A3, RELAT_1:46;
then reconsider f = b * (canFS S) as FinSequence by FINSEQ_1:def 2;
rng f c= rng b
by RELAT_1:45;
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
set cs = canFS (support b);
consider g being FinSequence of REAL such that
A8:
Sum b = Sum g
and
A9:
g = b * (canFS (support b))
by Def3;
len (canFS (support b)) = card (support b)
by Def1;
then A10:
dom (canFS (support b)) = Seg (card (support b))
by FINSEQ_1:def 3;
A11:
rng (canFS (support b)) = support b
by FUNCT_2:def 3;
then A12:
dom g = Seg (card (support b))
by A1, A5, A9, A10, RELAT_1:46, XBOOLE_1:1;
then A13:
len g = card (support b)
by FINSEQ_1:def 3;
A14:
card (support b) <= card S
by A1, NAT_1:44;
per cases
( card (support b) < card S or card (support b) = card S )
by A14, XXREAL_0:1;
suppose A15:
card (support b) < card S
;
:: thesis: Sum b = Sum fthen consider d being
Element of
NAT such that A16:
card S = (card (support b)) + d
and
1
<= d
by FSM_1:1;
set h =
d |-> 0 ;
len (d |-> 0 ) = d
by FINSEQ_1:def 18;
then A17:
dom (d |-> 0 ) = Seg d
by FINSEQ_1:def 3;
reconsider gr =
g as
FinSequence of
REAL ;
set F =
gr ^ (d |-> 0 );
len (gr ^ (d |-> 0 )) =
(len g) + (len (d |-> 0 ))
by FINSEQ_1:35
.=
card S
by A13, A16, FINSEQ_1:def 18
;
then A18:
dom (gr ^ (d |-> 0 )) = Seg (card S)
by FINSEQ_1:def 3;
set dd =
{ j where j is Element of NAT : ( j in dom f & f . j = 0 ) } ;
A19:
now consider x being
set such that A20:
( (
x in support b & not
x in S ) or (
x in S & not
x in support b ) )
by A15, TARSKI:2;
consider j being
set such that A21:
j in dom (canFS S)
and A22:
(canFS S) . j = x
by A1, A3, A20, FUNCT_1:def 5;
reconsider j =
j as
Element of
NAT by A21;
f . j = b . x
by A21, A22, FUNCT_1:23;
then
f . j = 0
by A1, A20, POLYNOM1:def 7;
then
j in { j where j is Element of NAT : ( j in dom f & f . j = 0 ) }
by A2, A6, A21;
hence
not
{ j where j is Element of NAT : ( j in dom f & f . j = 0 ) } is
empty
;
:: thesis: verum end; A23:
{ j where j is Element of NAT : ( j in dom f & f . j = 0 ) } c= dom f
then reconsider dd =
{ j where j is Element of NAT : ( j in dom f & f . j = 0 ) } as non
empty finite set by A19;
(
rng (canFS dd) = dd &
dd c= NAT )
by A23, 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 Th7;
reconsider cadd =
card dd as non
empty Element of
NAT ;
reconsider cdi =
cdi as
Function of
dd,
NAT by FUNCT_2:9;
set cSr =
(canFS S) | ((dom f) \ dd);
A25:
(canFS S) | ((dom f) \ dd) is
one-to-one
by FUNCT_1:84;
((findom f) \ dd) /\ (dom f) = (dom f) \ dd
by XBOOLE_1:28;
then A26:
dom ((canFS S) | ((dom f) \ dd)) = (dom f) \ dd
by A2, A6, RELAT_1:90;
then
rng ((canFS S) | ((dom f) \ dd)) = support b
by TARSKI:2;
then
support b,
(dom f) \ dd are_equipotent
by A25, A26, WELLORD2:def 4;
then A37:
card (support b) = card ((dom f) \ dd)
by CARD_1:21;
card ((dom f) \ dd) = (card (dom f)) - (card dd)
by A23, CARD_2:63;
then A38:
(card (support b)) + (card dd) = card S
by A6, A37, FINSEQ_1:78;
len cdd = card dd
by Def1;
then A39:
dom cdd = Seg d
by A16, A38, FINSEQ_1:def 3;
A40:
rng cdd = dd
by FUNCT_2:def 3;
A41:
dom cdi = dd
by FUNCT_2:def 1;
A44:
rng cdi = Seg d
by A39, FUNCT_1:55;
deffunc H1(
set )
-> Element of
NAT =
(cdi /. $1) + (card (support b));
consider z being
Function such that A45:
dom z = dd
and A46:
for
x being
set st
x in dd holds
z . x = H1(
x)
from FUNCT_1:sch 3();
A47:
rng z c= Seg (card S)
proof
let y be
set ;
:: 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
set such that A48:
x in dom z
and A49:
y = z . x
by FUNCT_1:def 5;
A50:
y = (cdi /. x) + (card (support b))
by A45, A46, A48, A49;
A51:
cdi /. x = cdi . x
by A41, A45, A48, PARTFUN1:def 8;
cdi . x in Seg d
by A41, A44, A45, A48, FUNCT_1:12;
then
( 1
<= cdi /. x &
cdi /. x <= d )
by A51, FINSEQ_1:3;
then
( 1
<= (cdi /. x) + (card (support b)) &
(cdi /. x) + (card (support b)) <= d + (card (support b)) )
by NAT_1:12, XREAL_1:8;
hence
y in Seg (card S)
by A16, A50, FINSEQ_1:3;
:: thesis: verum
end; set p =
(((canFS (support b)) " ) * (canFS S)) +* z;
A52:
dom ((((canFS (support b)) " ) * (canFS S)) +* z) = (dom (((canFS (support b)) " ) * (canFS S))) \/ (dom z)
by FUNCT_4:def 1;
then A62:
(dom (((canFS (support b)) " ) * (canFS S))) \/ (dom z) = dom (gr ^ (d |-> 0 ))
by TARSKI:2;
then A63:
dom ((((canFS (support b)) " ) * (canFS S)) +* z) = dom (gr ^ (d |-> 0 ))
by FUNCT_4:def 1;
then reconsider p =
(((canFS (support b)) " ) * (canFS S)) +* z as
Function of
(dom (gr ^ (d |-> 0 ))),
(dom (gr ^ (d |-> 0 ))) by A63, FUNCT_2:5;
A70:
p is
one-to-one
proof
let a,
c be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not a in dom p or not c in dom p or not p . a = p . c or a = c )
assume that A71:
a in dom p
and A72:
c in dom p
and A73:
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 A52, A71, A72, XBOOLE_0:def 3;
suppose A74:
(
a in dom (((canFS (support b)) " ) * (canFS S)) &
c in dom (((canFS (support b)) " ) * (canFS S)) )
;
:: thesis: a = cthen
not
a in dom z
by A53, XBOOLE_0:def 4;
then A75:
p . a =
(((canFS (support b)) " ) * (canFS S)) . a
by FUNCT_4:12
.=
((canFS (support b)) " ) . ((canFS S) . a)
by A74, FUNCT_1:22
;
not
c in dom z
by A53, A74, XBOOLE_0:def 4;
then A76:
p . c =
(((canFS (support b)) " ) * (canFS S)) . c
by FUNCT_4:12
.=
((canFS (support b)) " ) . ((canFS S) . c)
by A74, FUNCT_1:22
;
(canFS S) . a in dom ((canFS (support b)) " )
by A74, FUNCT_1:21;
then
(canFS S) . a in rng (canFS (support b))
by FUNCT_1:55;
then A77:
(canFS (support b)) . (((canFS (support b)) " ) . ((canFS S) . a)) = (canFS S) . a
by FUNCT_1:57;
(canFS S) . c in dom ((canFS (support b)) " )
by A74, FUNCT_1:21;
then
(canFS S) . c in rng (canFS (support b))
by FUNCT_1:55;
then A78:
((canFS S) " ) . ((canFS S) . a) = ((canFS S) " ) . ((canFS S) . c)
by A73, A75, A76, A77, FUNCT_1:57;
a in dom (canFS S)
by A74, FUNCT_1:21;
then A79:
((canFS S) " ) . ((canFS S) . a) = a
by FUNCT_1:56;
c in dom (canFS S)
by A74, FUNCT_1:21;
hence
a = c
by A78, A79, FUNCT_1:56;
:: thesis: verum end; suppose A80:
(
a in dom (((canFS (support b)) " ) * (canFS S)) &
c in dom z )
;
:: thesis: a = cthen A81:
p . c =
z . c
by FUNCT_4:14
.=
(cdi /. c) + (card (support b))
by A45, A46, A80
;
not
a in dom z
by A53, A80, XBOOLE_0:def 4;
then A82:
p . a =
(((canFS (support b)) " ) * (canFS S)) . a
by FUNCT_4:12
.=
((canFS (support b)) " ) . ((canFS S) . a)
by A80, FUNCT_1:22
;
(canFS S) . a in dom ((canFS (support b)) " )
by A80, FUNCT_1:21;
then
((canFS (support b)) " ) . ((canFS S) . a) in rng ((canFS (support b)) " )
by FUNCT_1:12;
then A83:
((canFS (support b)) " ) . ((canFS S) . a) in dom (canFS (support b))
by FUNCT_1:55;
(cdi /. c) + (card (support b)) <= 0 + (card (support b))
by A10, A73, A81, A82, A83, FINSEQ_1:3;
then
cdi /. c = 0
by XREAL_1:8;
then A84:
cdi . c = 0
by A41, A45, A80, PARTFUN1:def 8;
cdi . c in rng cdi
by A41, A45, A80, FUNCT_1:12;
hence
a = c
by A44, A84, FINSEQ_1:3;
:: thesis: verum end; suppose A85:
(
a in dom z &
c in dom (((canFS (support b)) " ) * (canFS S)) )
;
:: thesis: a = cthen A86:
p . a =
z . a
by FUNCT_4:14
.=
(cdi /. a) + (card (support b))
by A45, A46, A85
;
not
c in dom z
by A53, A85, XBOOLE_0:def 4;
then A87:
p . c =
(((canFS (support b)) " ) * (canFS S)) . c
by FUNCT_4:12
.=
((canFS (support b)) " ) . ((canFS S) . c)
by A85, FUNCT_1:22
;
(canFS S) . c in dom ((canFS (support b)) " )
by A85, FUNCT_1:21;
then
((canFS (support b)) " ) . ((canFS S) . c) in rng ((canFS (support b)) " )
by FUNCT_1:12;
then A88:
((canFS (support b)) " ) . ((canFS S) . c) in dom (canFS (support b))
by FUNCT_1:55;
(cdi /. a) + (card (support b)) <= 0 + (card (support b))
by A10, A73, A86, A87, A88, FINSEQ_1:3;
then
cdi /. a = 0
by XREAL_1:8;
then A89:
cdi . a = 0
by A41, A45, A85, PARTFUN1:def 8;
cdi . a in rng cdi
by A41, A45, A85, FUNCT_1:12;
hence
a = c
by A44, A89, FINSEQ_1:3;
:: thesis: verum end; suppose A90:
(
a in dom z &
c in dom z )
;
:: thesis: a = cthen A91:
p . a =
z . a
by FUNCT_4:14
.=
(cdi /. a) + (card (support b))
by A45, A46, A90
;
A92:
p . c =
z . c
by A90, FUNCT_4:14
.=
(cdi /. c) + (card (support b))
by A45, A46, A90
;
(
cdi /. a = cdi . a &
cdi /. c = cdi . c )
by A41, A45, A90, PARTFUN1:def 8;
hence
a = c
by A41, A45, A73, A90, A91, A92, FUNCT_1:def 8;
:: thesis: verum end;
end; now let x be
set ;
:: thesis: ( ( x in rng p implies x in dom (gr ^ (d |-> 0 )) ) & ( x in dom (gr ^ (d |-> 0 )) implies b1 in rng p ) )assume A100:
x in dom (gr ^ (d |-> 0 ))
;
:: thesis: b1 in rng pthen reconsider j =
x as
Element of
NAT ;
per cases
( j in dom gr or ex n being Nat st
( n in dom (d |-> 0 ) & j = (len gr) + n ) )
by A100, FINSEQ_1:38;
suppose A101:
j in dom gr
;
:: thesis: b1 in rng pthen A102:
(canFS (support b)) . j in support b
by A10, A11, A12, FUNCT_1:12;
then A103:
((canFS S) " ) . ((canFS (support b)) . j) in Seg (card S)
by A1, A2, A3, FUNCT_1:54;
then p . (((canFS S) " ) . ((canFS (support b)) . j)) =
(((canFS (support b)) " ) * (canFS S)) . (((canFS S) " ) . ((canFS (support b)) . j))
by FUNCT_4:12
.=
((canFS (support b)) " ) . ((canFS S) . (((canFS S) " ) . ((canFS (support b)) . j)))
by A2, A103, FUNCT_1:23
.=
((canFS (support b)) " ) . ((canFS (support b)) . j)
by A1, A3, A102, FUNCT_1:57
.=
j
by A10, A12, A101, FUNCT_1:56
;
hence
x in rng p
by A18, A63, A103, FUNCT_1:12;
:: thesis: verum end; suppose
ex
n being
Nat st
(
n in dom (d |-> 0 ) &
j = (len gr) + n )
;
:: thesis: b1 in rng pthen consider n being
Nat such that A106:
n in dom (d |-> 0 )
and A107:
j = (len gr) + n
;
A108:
cdd . n in dd
by A17, A39, A40, A106, FUNCT_1:12;
p . (cdd . n) =
z . (cdd . n)
by A17, A39, A40, A45, A106, FUNCT_1:12, FUNCT_4:14
.=
(cdi /. (cdd . n)) + (card (support b))
by A17, A39, A40, A46, A106, FUNCT_1:12
.=
(cdi . (cdd . n)) + (card (support b))
by A17, A39, A40, A41, A106, FUNCT_1:12, PARTFUN1:def 8
.=
n + (card (support b))
by A17, A39, A106, FUNCT_1:56
.=
j
by A12, A107, FINSEQ_1:def 3
;
hence
x in rng p
by A6, A18, A23, A63, A108, FUNCT_1:12;
:: thesis: verum end; end; then A109:
rng p = dom (gr ^ (d |-> 0 ))
by TARSKI:2;
then B110:
p is
onto
by FUNCT_2:def 3;
A111:
dom ((gr ^ (d |-> 0 )) * p) = dom (gr ^ (d |-> 0 ))
by A63, A109, RELAT_1:46;
now let x be
set ;
:: thesis: ( x in dom f implies f . b1 = ((gr ^ (d |-> 0 )) * p) . b1 )assume A112:
x in dom f
;
:: thesis: f . b1 = ((gr ^ (d |-> 0 )) * p) . b1per cases
( f . x = 0 or f . x <> 0 )
;
suppose A113:
f . x = 0
;
:: thesis: f . b1 = ((gr ^ (d |-> 0 )) * p) . b1reconsider j =
x as
Element of
NAT by A112;
A114:
j in dom z
by A45, A112, A113;
then A115:
p . x =
z . x
by FUNCT_4:14
.=
(cdi /. x) + (card (support b))
by A45, A46, A114
;
reconsider px =
p . x as
Element of
NAT ;
dom cdi = dd
by FUNCT_2:def 1;
then A116:
cdi /. x = cdi . x
by A45, A114, PARTFUN1:def 8;
A117:
cdi . x in Seg (card dd)
by A45, A114, FUNCT_2:7;
reconsider cdix =
cdi /. x as
Element of
NAT ;
thus f . x =
(d |-> 0 ) . cdix
by A16, A38, A45, A113, A114, A116, FUNCOP_1:13, FUNCT_2:7
.=
(gr ^ (d |-> 0 )) . px
by A13, A16, A17, A38, A115, A116, A117, FINSEQ_1:def 7
.=
((gr ^ (d |-> 0 )) * p) . x
by A6, A18, A111, A112, FUNCT_1:22
;
:: thesis: verum end; suppose A118:
f . x <> 0
;
:: thesis: f . b1 = ((gr ^ (d |-> 0 )) * p) . b1
f . x = b . ((canFS S) . x)
by A112, FUNCT_1:22;
then
(canFS S) . x in support b
by A118, POLYNOM1:def 7;
then A120:
(canFS S) . x in rng (canFS (support b))
by FUNCT_2:def 3;
then A121:
((canFS (support b)) " ) . ((canFS S) . x) in dom (canFS (support b))
by FUNCT_1:54;
A122:
p . x =
(((canFS (support b)) " ) * (canFS S)) . x
by A45, A119, FUNCT_4:12
.=
((canFS (support b)) " ) . ((canFS S) . x)
by A2, A6, A112, FUNCT_1:23
;
reconsider px =
p . x as
Element of
NAT ;
thus f . x =
b . ((canFS S) . x)
by A112, FUNCT_1:22
.=
b . ((canFS (support b)) . px)
by A120, A122, FUNCT_1:54
.=
g . px
by A9, A121, A122, FUNCT_1:23
.=
(gr ^ (d |-> 0 )) . px
by A10, A12, A121, A122, FINSEQ_1:def 7
.=
((gr ^ (d |-> 0 )) * p) . x
by A6, A18, A111, A112, FUNCT_1:22
;
:: thesis: verum end; end; then A123:
f = (gr ^ (d |-> 0 )) * p
by A5, A18, A111, A2, A3, FUNCT_1:9, RELAT_1:46;
Sum (d |-> 0 ) = 0
by RVSUM_1:111;
then Sum gr =
(Sum gr) + (Sum (d |-> 0 ))
.=
Sum (gr ^ (d |-> 0 ))
by RVSUM_1:105
;
hence
Sum b = Sum f
by A8, B110, A123, A70, FINSOP_1:8;
:: thesis: verum end;