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 ]
proof
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 ; :: thesis: verum
end;
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; :: thesis: S1[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 ;
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 ;
A16: f = fk ^ <*(f . (k + 1))*> by ;
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 ;
then A18: card Zk = k by ;
reconsider Xk = union Zk as finite set ;
A19: now :: thesis: Zk is a_partition of Xk
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 ) ) )
proof
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 )
proof
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 ; :: thesis: verum
end;
hence ( a <> {} & ( for b being Subset of Xk holds
( not b in Zk or a = b or a misses b ) ) ) by A22; :: thesis: verum
end;
Zk c= bool (union Zk) by ZFMISC_1:82;
hence Zk is a_partition of Xk by ; :: thesis: verum
end;
reconsider ck = c | (Seg k) as FinSequence of NAT by FINSEQ_1:18;
A25: len ck = len fk by ;
for i being Element of NAT st i in dom ck holds
ck . i = card (fk . i)
proof
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 ;
then A28: dom ck = dom fk by ;
A29: dom ck c= dom c by RELAT_1:60;
ck . i = c . i by ;
then ck . i = card (f . i) by ;
hence ck . i = card (fk . i) by ; :: thesis: verum
end;
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 ; :: 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 ;
consider i being Nat such that
A34: i in dom fk and
A35: fk . i = x by ;
now :: thesis: not fk . i = fk1
assume A36: fk . i = fk1 ; :: thesis: contradiction
A37: dom fk = Seg k by ;
A38: i in Seg k by ;
i <= k by ;
then A39: i < k + 1 by NAT_1:13;
A40: dom f = Seg (k + 1) by ;
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 ;
fk . i = f . i by ;
hence contradiction by A9, A36, A38, A39, A40, A41, A42; :: thesis: verum
end;
hence x misses fk1 by ; :: thesis: 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 ;
then reconsider fk1 = fk1 as finite set ;
A44: Z = (rng fk) \/ (rng <*fk1*>) by
.= Zk \/ {fk1} by FINSEQ_1:39 ;
A45: X = union Z by EQREL_1:def 4
.= (union Zk) \/ (union {fk1}) by
.= Xk \/ fk1 by ZFMISC_1:25 ;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A46: k + 1 in dom c by ;
rng ck c= REAL ;
then reconsider ckc = ck as FinSequence of REAL by FINSEQ_1:def 4;
card X = (Sum ck) + (card fk1) by
.= (Sum ck) + (c . (k + 1)) by
.= Sum (ckc ^ <*(c . (k + 1))*>) by RVSUM_1:74
.= Sum c by ;
hence card X = Sum c ; :: thesis: verum
end;
A47: for k being Nat holds S1[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