defpred S₁[ 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₁[ 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 A5, RVSUM_1:72; :: thesis: verum

end;

A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[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 ;

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 A24, EQREL_1:def 4; :: 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 A20, EQREL_1:def 4; :: thesis: verum

end;

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)

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 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;

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

assume 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;

hence x misses fk1 by A10, A32, A33, A35, EQREL_1:def 4; :: 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 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;

A47: for k being Nat holds S₁[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