defpred S1[ Element of NAT ] means for X being finite set
for z being a_partition of X st card z = $1 holds
for f being FinSequence of z st f is one-to-one & rng f = z holds
for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card X = Sum c;
A1:
S1[ 0 ]
A6:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A7:
S1[
k]
;
S1[k + 1]
let X be
finite set ;
for z being a_partition of X st card z = k + 1 holds
for f being FinSequence of z st f is one-to-one & rng f = z holds
for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card X = Sum clet Z be
a_partition of
X;
( card Z = k + 1 implies for f being FinSequence of Z st f is one-to-one & rng f = Z holds
for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card X = Sum c )
assume A8:
card Z = k + 1
;
for f being FinSequence of Z st f is one-to-one & rng f = Z holds
for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card X = Sum c
let f be
FinSequence of
Z;
( f is one-to-one & rng f = Z implies for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card X = Sum c )
assume that A9:
f is
one-to-one
and A10:
rng f = Z
;
for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card X = Sum c
let c be
FinSequence of
NAT ;
( len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) implies card X = Sum c )
assume that A11:
len c = len f
and A12:
for
i being
Element of
NAT st
i in dom c holds
c . i = card (f . i)
;
card X = Sum c
A13:
len f = k + 1
by A8, A9, A10, FINSEQ_4:77;
A14:
Z <> {}
by A8;
reconsider Z =
Z as non
empty set by A8;
reconsider f =
f as
FinSequence of
Z ;
reconsider X =
X as non
empty finite set by A14, EQREL_1:41;
reconsider fk =
f | (Seg k) as
FinSequence of
Z by FINSEQ_1:23;
A15:
len fk = k
by A13, FINSEQ_3:59;
A16:
f = fk ^ <*(f . (k + 1))*>
by A13, FINSEQ_3:61;
reconsider Zk =
rng fk as
finite set ;
union Zk c= union Z
by ZFMISC_1:95;
then A17:
union Zk c= X
by EQREL_1:def 6;
reconsider fk =
fk as
FinSequence of
Zk by FINSEQ_1:def 4;
A18:
fk is
one-to-one
by A9, FUNCT_1:84;
then A19:
card Zk = k
by A15, FINSEQ_4:77;
reconsider Xk =
union Zk as
finite set by A17;
reconsider ck =
c | (Seg k) as
FinSequence of
NAT by FINSEQ_1:23;
A27:
len ck = len fk
by A11, A13, A15, FINSEQ_3:59;
for
i being
Element of
NAT st
i in dom ck holds
ck . i = card (fk . i)
then A32:
card Xk = Sum ck
by A7, A18, A19, A20, A27;
reconsider fk1 =
f . (k + 1) as
set ;
for
x being
set st
x in Zk holds
x misses fk1
proof
let x be
set ;
( x in Zk implies x misses fk1 )
assume A33:
x in Zk
;
x misses fk1
A34:
x in Z
by A33;
dom f = Seg (len f)
by FINSEQ_1:def 3;
then A35:
fk1 in rng f
by A13, FINSEQ_1:6, FUNCT_1:12;
consider i being
Nat such that A36:
i in dom fk
and A37:
fk . i = x
by A33, FINSEQ_2:11;
now assume A38:
fk . i = fk1
;
contradictionA39:
dom fk = Seg k
by A15, FINSEQ_1:def 3;
A40:
i in Seg k
by A15, A36, FINSEQ_1:def 3;
i <= k
by A36, A39, FINSEQ_1:3;
then A41:
i < k + 1
by NAT_1:13;
A42:
dom f = Seg (k + 1)
by A13, FINSEQ_1:def 3;
k <= k + 1
by NAT_1:12;
then A43:
Seg k c= Seg (k + 1)
by FINSEQ_1:7;
A44:
k + 1
in dom f
by A42, FINSEQ_1:6;
fk . i = f . i
by A36, FUNCT_1:70;
hence
contradiction
by A9, A38, A40, A41, A42, A43, A44, FUNCT_1:def 8;
verum end;
hence
x misses fk1
by A10, A34, A35, A37, EQREL_1:def 6;
verum
end;
then A45:
fk1 misses Xk
by ZFMISC_1:98;
A46:
union Z = X
by EQREL_1:def 6;
dom f = Seg (len f)
by FINSEQ_1:def 3;
then
fk1 in rng f
by A13, FINSEQ_1:6, FUNCT_1:12;
then reconsider fk1 =
fk1 as
finite set by A46, FINSET_1:25;
A47:
Z =
(rng fk) \/ (rng <*fk1*>)
by A10, A16, FINSEQ_1:44
.=
Zk \/ {fk1}
by FINSEQ_1:56
;
A48:
X =
union Z
by EQREL_1:def 6
.=
(union Zk) \/ (union {fk1})
by A47, ZFMISC_1:96
.=
Xk \/ fk1
by ZFMISC_1:31
;
k + 1
in Seg (k + 1)
by FINSEQ_1:6;
then A49:
k + 1
in dom c
by A11, A13, FINSEQ_1:def 3;
rng ck c= REAL
;
then reconsider ckc =
ck as
FinSequence of
REAL by FINSEQ_1:def 4;
card X =
(Sum ck) + (card fk1)
by A32, A45, A48, CARD_2:53
.=
(Sum ck) + (c . (k + 1))
by A12, A49
.=
Sum (ckc ^ <*(c . (k + 1))*>)
by RVSUM_1:104
.=
Sum c
by A11, A13, FINSEQ_3:61
;
hence
card X = Sum c
;
verum
end;
A50:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A1, A6);
let X be finite set ; for Y being a_partition of X
for f being FinSequence of Y st f is one-to-one & rng f = Y holds
for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card X = Sum c
let Y be a_partition of X; for f being FinSequence of Y st f is one-to-one & rng f = Y holds
for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card X = Sum c
card Y = card Y
;
hence
for f being FinSequence of Y st f is one-to-one & rng f = Y holds
for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card X = Sum c
by A50; verum