defpred S₁[ Nat] means for S being Function
for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & $1 = len L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) holds
( Union S is finite & card (Union S) = Sum L );

A1: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]

now

let S be Function; :: thesis: for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & n + 1 = len L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) holds
( Union S is finite & card (Union S) = Sum L )
let L be FinSequence of NAT ; :: thesis: ( S is disjoint_valued & dom S = dom L & n + 1 = len L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) implies ( Union S is finite & card (Union S) = Sum L ) )
assume that
A3: S is disjoint_valued and
A4: dom S = dom L and
A5: n + 1 = len L and
A6: for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ; :: thesis: ( Union S is finite & card (Union S) = Sum L )
reconsider SN = S | (Seg n) as Function ;
reconsider LN = L | n as FinSequence of NAT ;
A7: n = len LN by A5, FINSEQ_1:59, NAT_1:12;

now

let x be set ; :: thesis: ( x in Union S implies x in (Union SN) \/ (S . (n + 1)) )
assume x in Union S ; :: thesis: x in (Union SN) \/ (S . (n + 1))
then consider y being set such that
A8: x in y and
A9: y in rng S by TARSKI:def 4;
consider i being set such that
A10: i in dom S and
A11: y = S . i by A9, FUNCT_1:def 3;
A12: i in Seg (n + 1) by A4, A5, A10, FINSEQ_1:def 3;
reconsider i = i as Element of NAT by A4, A10;
A13: i <= n + 1 by A12, FINSEQ_1:1;
A14: 1 <= i by A12, FINSEQ_1:1;

now

per cases ( i = n + 1 or i <> n + 1 ) ;

suppose i = n + 1 ; :: thesis: x in (Union SN) \/ (S . (n + 1))

hence x in (Union SN) \/ (S . (n + 1)) by A8, A11, XBOOLE_0:def 3; :: thesis: verum

end;

suppose i <> n + 1 ; :: thesis: x in (Union SN) \/ (S . (n + 1))

then i < n + 1 by A13, XXREAL_0:1;
then i <= n by NAT_1:13;
then i in Seg n by A14;
then i in (dom S) /\ (Seg n) by A10, XBOOLE_0:def 4;
then A15: i in dom SN by RELAT_1:61;
then S . i = SN . i by FUNCT_1:47;
then y in rng SN by A11, A15, FUNCT_1:def 3;
then x in Union SN by A8, TARSKI:def 4;
hence x in (Union SN) \/ (S . (n + 1)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in (Union SN) \/ (S . (n + 1)) ; :: thesis: verum

end;

then A16: Union S c= (Union SN) \/ (S . (n + 1)) by TARSKI:def 3;
A17: (Union SN) \/ (S . (n + 1)) c= Union S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Union SN) \/ (S . (n + 1)) or x in Union S )
assume A18: x in (Union SN) \/ (S . (n + 1)) ; :: thesis: x in Union S

now

per cases ( x in S . (n + 1) or x in Union SN ) by A18, XBOOLE_0:def 3;

suppose A19: x in S . (n + 1) ; :: thesis: x in Union S

n + 1 in Seg (n + 1) by FINSEQ_1:4;
then n + 1 in dom S by A4, A5, FINSEQ_1:def 3;
then S . (n + 1) in rng S by FUNCT_1:def 3;
hence x in Union S by A19, TARSKI:def 4; :: thesis: verum

end;

suppose x in Union SN ; :: thesis: x in Union S

then consider y being set such that
A20: x in y and
A21: y in rng SN by TARSKI:def 4;
consider i being set such that
A22: i in dom SN and
A23: y = SN . i by A21, FUNCT_1:def 3;
i in (dom S) /\ (Seg n) by A22, RELAT_1:61;
then A24: i in dom S by XBOOLE_0:def 4;
SN . i = S . i by A22, FUNCT_1:47;
then y in rng S by A23, A24, FUNCT_1:def 3;
hence x in Union S by A20, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence x in Union S ; :: thesis: verum

end;

then A25: (Union SN) \/ (S . (n + 1)) = Union S by A16, XBOOLE_0:def 10;
A26: for i being Nat st i in dom SN holds
( SN . i is finite & LN . i = card (SN . i) )

proof

let i be Nat; :: thesis: ( i in dom SN implies ( SN . i is finite & LN . i = card (SN . i) ) )
assume A27: i in dom SN ; :: thesis: ( SN . i is finite & LN . i = card (SN . i) )
then A28: i in (dom S) /\ (Seg n) by RELAT_1:61;
then A29: i in dom S by XBOOLE_0:def 4;
LN . i = L . i by A4, A28, FUNCT_1:48
.= card (S . i) by A6, A29
.= card (SN . i) by A27, FUNCT_1:47 ;
hence ( SN . i is finite & LN . i = card (SN . i) ) ; :: thesis: verum

end;

now

let x, y be set ; :: thesis: ( x <> y implies SN . b₁ misses SN . b₂ )
assume A30: x <> y ; :: thesis: SN . b₁ misses SN . b₂

per cases ( ( x in dom SN & y in dom SN ) or not x in dom SN or not y in dom SN ) ;

suppose ( x in dom SN & y in dom SN ) ; :: thesis: SN . b₁ misses SN . b₂

then ( SN . x = S . x & SN . y = S . y ) by FUNCT_1:47;
hence SN . x misses SN . y by A3, A30, PROB_2:def 2; :: thesis: verum

end;

suppose A31: ( not x in dom SN or not y in dom SN ) ; :: thesis: SN . b₁ misses SN . b₂

now

per cases ( not x in dom SN or not y in dom SN ) by A31;

suppose not x in dom SN ; :: thesis: SN . x misses SN . y

then SN . x = {} by FUNCT_1:def 2;
then (SN . x) /\ (SN . y) = {} ;
hence SN . x misses SN . y by XBOOLE_0:def 7; :: thesis: verum

end;

suppose not y in dom SN ; :: thesis: SN . x misses SN . y

then SN . y = {} by FUNCT_1:def 2;
then (SN . x) /\ (SN . y) = {} ;
hence SN . x misses SN . y by XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

hence SN . x misses SN . y ; :: thesis: verum

end;

end;

end;

then A32: SN is disjoint_valued by PROB_2:def 2;
A33: dom SN = (dom S) /\ (Seg n) by RELAT_1:61
.= dom LN by A4, RELAT_1:61 ;
then A34: card (Union SN) = Sum LN by A2, A32, A7, A26;
reconsider USN = Union SN as finite set by A2, A32, A33, A7, A26;
A35: 1 <= n + 1 by NAT_1:11;
A36: L = (L | n) ^ <*(L /. (len L))*> by A5, FINSEQ_5:21
.= LN ^ <*(L . (n + 1))*> by A5, A35, FINSEQ_4:15 ;
n + 1 in Seg (len L) by A5, FINSEQ_1:4;
then A37: n + 1 in dom S by A4, FINSEQ_1:def 3;
then reconsider S1 = S . (n + 1) as finite set by A6;
Union S = USN \/ S1 by A16, A17, XBOOLE_0:def 10;
hence Union S is finite ; :: thesis: card (Union S) = Sum L
for z being set st z in rng SN holds
z misses S . (n + 1)

proof

let y be set ; :: thesis: ( y in rng SN implies y misses S . (n + 1) )
assume y in rng SN ; :: thesis: y misses S . (n + 1)
then consider i being set such that
A38: i in dom SN and
A39: y = SN . i by FUNCT_1:def 3;
A40: i in (dom S) /\ (Seg n) by A38, RELAT_1:61;
then A41: i in Seg n by XBOOLE_0:def 4;
reconsider i = i as Element of NAT by A40;
i <= n by A41, FINSEQ_1:1;
then A42: i <> n + 1 by NAT_1:13;
y = S . i by A38, A39, FUNCT_1:47;
hence y misses S . (n + 1) by A3, A42, PROB_2:def 2; :: thesis: verum

end;

then Union SN misses S . (n + 1) by ZFMISC_1:80;
then card ((Union SN) \/ (S . (n + 1))) = (card USN) + (card S1) by CARD_2:40;
hence card (Union S) = (Sum LN) + (L . (n + 1)) by A6, A37, A34, A25
.= Sum L by A36, RVSUM_1:74 ;
:: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A43: S₁[ 0 ]

proof

let S be Function; :: thesis: for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & 0 = len L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) holds
( Union S is finite & card (Union S) = Sum L )
let L be FinSequence of NAT ; :: thesis: ( S is disjoint_valued & dom S = dom L & 0 = len L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) implies ( Union S is finite & card (Union S) = Sum L ) )
assume that
S is disjoint_valued and
A44: dom S = dom L and
A45: 0 = len L and
for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ; :: thesis: ( Union S is finite & card (Union S) = Sum L )
A46: L = {} by A45;
then S = {} by A44;
then for X being set st X in rng S holds
X c= {} ;
then Union S c= {} by ZFMISC_1:76;
hence ( Union S is finite & card (Union S) = Sum L ) by A46, RVSUM_1:72; :: thesis: verum

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A43, A1); :: thesis: verum