defpred S_{1}[ 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: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A1, A6);

let X be finite set ; :: thesis: 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; :: thesis: 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; :: thesis: verum

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

proof

A6:
for k being Nat st S
let X be finite set ; :: thesis: for z being a_partition of X st card z = 0 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

let z be a_partition of X; :: thesis: ( card z = 0 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 A2: card z = 0 ; :: thesis: 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; :: thesis: ( 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

f is one-to-one and

rng f = z ; :: thesis: 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 ; :: thesis: ( 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

A3: len c = len f and

for i being Element of NAT st i in dom c holds

c . i = card (f . i) ; :: thesis: card X = Sum c

A4: z = {} by A2;

A5: X = {} by A2;

c = {} by A3, A4;

hence card X = Sum c by A5, RVSUM_1:72; :: thesis: verum

end;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 z be a_partition of X; :: thesis: ( card z = 0 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 A2: card z = 0 ; :: thesis: 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; :: thesis: ( 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

f is one-to-one and

rng f = z ; :: thesis: 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 ; :: thesis: ( 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

A3: len c = len f and

for i being Element of NAT st i in dom c holds

c . i = card (f . i) ; :: thesis: card X = Sum c

A4: z = {} by A2;

A5: X = {} by A2;

c = {} by A3, A4;

hence card X = Sum c by A5, RVSUM_1:72; :: thesis: verum

S

proof

A47:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A7: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let X be finite set ; :: thesis: 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 c

let Z be a_partition of X; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: 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 ;

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)

reconsider fk1 = f . (k + 1) as set ;

for x being set st x in Zk holds

x misses fk1

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

end;assume A7: S

let X be finite set ; :: thesis: 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 c

let Z be a_partition of X; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: 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 ;

A19: now :: thesis: Zk is a_partition of Xk

reconsider ck = c | (Seg k) as FinSequence of NAT by FINSEQ_1:18;A20:
for a being Subset of Xk st a in Zk holds

( a <> {} & ( for b being Subset of Xk holds

( not b in Zk or a = b or a misses b ) ) )

hence Zk is a_partition of Xk by A20, EQREL_1:def 4; :: thesis: verum

end;( a <> {} & ( for b being Subset of Xk holds

( not b in Zk or a = b or a misses b ) ) )

proof

Zk c= bool (union Zk)
by ZFMISC_1:82;
let a be Subset of Xk; :: thesis: ( a in Zk implies ( a <> {} & ( for b being Subset of Xk holds

( not b in Zk or a = b or a misses b ) ) ) )

assume A21: a in Zk ; :: thesis: ( a <> {} & ( for b being Subset of Xk holds

( not b in Zk or a = b or a misses b ) ) )

A22: a in Z by A21;

for b being Subset of Xk holds

( not b in Zk or a = b or a misses b )

( not b in Zk or a = b or a misses b ) ) ) by A22; :: thesis: verum

end;( not b in Zk or a = b or a misses b ) ) ) )

assume A21: a in Zk ; :: thesis: ( a <> {} & ( for b being Subset of Xk holds

( not b in Zk or a = b or a misses b ) ) )

A22: a in Z by A21;

for b being Subset of Xk holds

( not b in Zk or a = b or a misses b )

proof

hence
( a <> {} & ( for b being Subset of Xk holds
let b be Subset of Xk; :: thesis: ( not b in Zk or a = b or a misses b )

assume A23: b in Zk ; :: thesis: ( a = b or a misses b )

A24: a in Z by A21;

b in Z by A23;

hence ( a = b or a misses b ) by A24, EQREL_1:def 4; :: thesis: verum

end;assume A23: b in Zk ; :: thesis: ( a = b or a misses b )

A24: a in Z by A21;

b in Z by A23;

hence ( a = b or a misses b ) by A24, EQREL_1:def 4; :: thesis: verum

( not b in Zk or a = b or a misses b ) ) ) by A22; :: thesis: verum

hence Zk is a_partition of Xk by A20, EQREL_1:def 4; :: thesis: verum

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)

proof

then A30:
card Xk = Sum ck
by A7, A17, A18, A19, A25;
let i be Element of NAT ; :: thesis: ( i in dom ck implies ck . i = card (fk . i) )

assume A26: i in dom ck ; :: thesis: ck . i = card (fk . i)

A27: k <= k + 1 by NAT_1:11;

then dom ck = Seg k by A11, A13, FINSEQ_1:17;

then A28: dom ck = dom fk by A13, A27, FINSEQ_1:17;

A29: dom ck c= dom c by RELAT_1:60;

ck . i = c . i by A26, FUNCT_1:47;

then ck . i = card (f . i) by A12, A26, A29;

hence ck . i = card (fk . i) by A26, A28, FUNCT_1:47; :: thesis: verum

end;assume A26: i in dom ck ; :: thesis: ck . i = card (fk . i)

A27: k <= k + 1 by NAT_1:11;

then dom ck = Seg k by A11, A13, FINSEQ_1:17;

then A28: dom ck = dom fk by A13, A27, FINSEQ_1:17;

A29: dom ck c= dom c by RELAT_1:60;

ck . i = c . i by A26, FUNCT_1:47;

then ck . i = card (f . i) by A12, A26, A29;

hence ck . i = card (fk . i) by A26, A28, FUNCT_1:47; :: thesis: verum

reconsider fk1 = f . (k + 1) as set ;

for x being set st x in Zk holds

x misses fk1

proof

then A43:
fk1 misses Xk
by ZFMISC_1:80;
let x be set ; :: thesis: ( x in Zk implies x misses fk1 )

assume A31: x in Zk ; :: thesis: 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;

end;assume A31: x in Zk ; :: thesis: 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 :: thesis: not fk . i = fk1

hence
x misses fk1
by A10, A32, A33, A35, EQREL_1:def 4; :: thesis: verumassume A36:
fk . i = fk1
; :: thesis: contradiction

A37: 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; :: thesis: verum

end;A37: 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; :: thesis: verum

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

let X be finite set ; :: thesis: 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; :: thesis: 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; :: thesis: verum