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 (rng S) is finite & card (union (rng 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 (rng S) is finite & card (union (rng 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 (rng S) is finite & card (union (rng 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 (rng S) is finite & card (union (rng 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:80, NAT_1:12;

now

let x be set ; :: thesis: ( x in union (rng S) implies x in (union (rng SN)) \/ (S . (n + 1)) )
assume x in union (rng S) ; :: thesis: x in (union (rng 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 5;
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:3;
A14: 1 <= i by A12, FINSEQ_1:3;

now

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

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

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

end;

suppose i <> n + 1 ; :: thesis: x in (union (rng 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:90;
then S . i = SN . i by FUNCT_1:70;
then y in rng SN by A11, A15, FUNCT_1:def 5;
then x in union (rng SN) by A8, TARSKI:def 4;
hence x in (union (rng SN)) \/ (S . (n + 1)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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

end;

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

proof

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

now

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

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

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

end;

suppose x in union (rng SN) ; :: thesis: x in union (rng 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 5;
i in (dom S) /\ (Seg n) by A22, RELAT_1:90;
then A24: i in dom S by XBOOLE_0:def 4;
SN . i = S . i by A22, FUNCT_1:70;
then y in rng S by A23, A24, FUNCT_1:def 5;
hence x in union (rng S) by A20, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence x in union (rng S) ; :: thesis: verum

end;

then A25: (union (rng SN)) \/ (S . (n + 1)) = union (rng 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:90;
then A29: i in dom S by XBOOLE_0:def 4;
LN . i = L . i by A4, A28, FUNCT_1:71
.= card (S . i) by A6, A29
.= card (SN . i) by A27, FUNCT_1:70 ;
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:70;
hence SN . x misses SN . y by A3, A30, PROB_2:def 3; :: 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 4;
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 4;
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 3;
A33: dom SN = (dom S) /\ (Seg n) by RELAT_1:90
.= dom LN by A4, RELAT_1:90 ;
then A34: card (union (rng SN)) = Sum LN by A2, A32, A7, A26;
reconsider USN = union (rng 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:24
.= LN ^ <*(L . (n + 1))*> by A5, A35, FINSEQ_4:24 ;
n + 1 in Seg (len L) by A5, FINSEQ_1:6;
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 (rng S) = USN \/ S1 by A16, A17, XBOOLE_0:def 10;
hence union (rng S) is finite ; :: thesis: card (union (rng 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 5;
A40: i in (dom S) /\ (Seg n) by A38, RELAT_1:90;
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:3;
then A42: i <> n + 1 by NAT_1:13;
y = S . i by A38, A39, FUNCT_1:70;
hence y misses S . (n + 1) by A3, A42, PROB_2:def 3; :: thesis: verum

end;

then union (rng SN) misses S . (n + 1) by ZFMISC_1:98;
then card ((union (rng SN)) \/ (S . (n + 1))) = (card USN) + (card S1) by CARD_2:53;
hence card (union (rng S)) = (Sum LN) + (L . (n + 1)) by A6, A37, A34, A25
.= Sum L by A36, RVSUM_1:104 ;
:: 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 (rng S) is finite & card (union (rng 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 (rng S) is finite & card (union (rng 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 (rng S) is finite & card (union (rng 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 (rng S) c= {} by ZFMISC_1:94;
hence ( union (rng S) is finite & card (union (rng S)) = Sum L ) by A46, RVSUM_1:102; :: thesis: verum

end;

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