defpred S1[ 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 Nat st S1[k] holds
S1[k + 1]
proof
let k be
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:62;
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;
reconsider fk =
f | (Seg k) as
FinSequence of
Z by FINSEQ_1:18;
A15:
len fk = k
by A13, FINSEQ_3:53;
A16:
f = fk ^ <*(f . (k + 1))*>
by A13, FINSEQ_3:55;
reconsider Zk =
rng fk as
finite set ;
reconsider fk =
fk as
FinSequence of
Zk by FINSEQ_1:def 4;
A17:
fk is
one-to-one
by A9, FUNCT_1:52;
then A18:
card Zk = k
by A15, FINSEQ_4:62;
reconsider Xk =
union Zk as
finite set ;
reconsider ck =
c | (Seg k) as
FinSequence of
NAT by FINSEQ_1:18;
A25:
len ck = len fk
by A11, A13, A15, FINSEQ_3:53;
for
i being
Element of
NAT st
i in dom ck holds
ck . i = card (fk . i)
then A30:
card Xk = Sum ck
by A7, A17, A18, A19, A25;
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 A31:
x in Zk
;
x misses fk1
A32:
x in Z
by A31;
dom f = Seg (len f)
by FINSEQ_1:def 3;
then A33:
fk1 in rng f
by A13, FINSEQ_1:4, FUNCT_1:3;
consider i being
Nat such that A34:
i in dom fk
and A35:
fk . i = x
by A31, FINSEQ_2:10;
now not fk . i = fk1assume A36:
fk . i = fk1
;
contradictionA37:
dom fk = Seg k
by A15, FINSEQ_1:def 3;
A38:
i in Seg k
by A15, A34, FINSEQ_1:def 3;
i <= k
by A34, A37, FINSEQ_1:1;
then A39:
i < k + 1
by NAT_1:13;
A40:
dom f = Seg (k + 1)
by A13, FINSEQ_1:def 3;
k <= k + 1
by NAT_1:12;
then A41:
Seg k c= Seg (k + 1)
by FINSEQ_1:5;
A42:
k + 1
in dom f
by A40, FINSEQ_1:4;
fk . i = f . i
by A34, FUNCT_1:47;
hence
contradiction
by A9, A36, A38, A39, A40, A41, A42;
verum end;
hence
x misses fk1
by A10, A32, A33, A35, EQREL_1:def 4;
verum
end;
then A43:
fk1 misses Xk
by ZFMISC_1:80;
dom f = Seg (len f)
by FINSEQ_1:def 3;
then
fk1 in rng f
by A13, FINSEQ_1:4, FUNCT_1:3;
then reconsider fk1 =
fk1 as
finite set ;
A44:
Z =
(rng fk) \/ (rng <*fk1*>)
by A10, A16, FINSEQ_1:31
.=
Zk \/ {fk1}
by FINSEQ_1:39
;
A45:
X =
union Z
by EQREL_1:def 4
.=
(union Zk) \/ (union {fk1})
by A44, ZFMISC_1:78
.=
Xk \/ fk1
by ZFMISC_1:25
;
k + 1
in Seg (k + 1)
by FINSEQ_1:4;
then A46:
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 A30, A43, A45, CARD_2:40
.=
(Sum ck) + (c . (k + 1))
by A12, A46
.=
Sum (ckc ^ <*(c . (k + 1))*>)
by RVSUM_1:74
.=
Sum c
by A11, A13, FINSEQ_3:55
;
hence
card X = Sum c
;
verum
end;
A47:
for k being Nat holds S1[k]
from NAT_1:sch 2(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 A47; verum