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 );
P0: 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 AS0: ( 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) ) ) ) ; :: thesis: ( union (rng S) is finite & card (union (rng S)) = Sum L )
P0: L = {} by AS0;
then S = {} by AS0;
then for X being set st X in rng S holds
X c= {} ;
then P3P: union (rng S) c= {} by ZFMISC_1:94;
thus ( union (rng S) is finite & card (union (rng S)) = Sum L ) by P3P, P0, RVSUM_1:102; :: thesis: verum

end;

PN: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume P1: 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 ASN: ( 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) ) ) ) ; :: 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 ;
n + 1 in Seg (len L) by ASN, FINSEQ_1:6;
then Q0: n + 1 in dom S by ASN, FINSEQ_1:def 3;
Q1: SN is disjoint_valued

proof

now

let x, y be set ; :: thesis: ( x <> y implies SN . b₁ misses SN . b₂ )
assume A1: 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 A1, ASN, PROB_2:def 3; :: thesis: verum

end;

suppose A12: ( 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 A12;

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;

hence SN is disjoint_valued by PROB_2:def 3; :: thesis: verum

end;

Q2: dom SN = (dom S) /\ (Seg n) by RELAT_1:90
.= dom LN by RELAT_1:90, ASN ;
Q3: n = len LN by FINSEQ_1:80, ASN, NAT_1:12;
Q4: 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 A2P: i in dom SN ; :: thesis: ( SN . i is finite & LN . i = card (SN . i) )
then A2: i in (dom S) /\ (Seg n) by RELAT_1:90;
then A3: ( i in dom S & i in Seg n ) by XBOOLE_0:def 4;
LN . i = L . i by FUNCT_1:71, ASN, A2
.= card (S . i) by ASN, A3
.= card (SN . i) by A2P, FUNCT_1:70 ;
hence ( SN . i is finite & LN . i = card (SN . i) ) ; :: thesis: verum

end;

Q5: ( union (rng SN) is finite & card (union (rng SN)) = Sum LN ) by P1, Q1, Q2, Q3, Q4;
Q6: (union (rng SN)) \/ (S . (n + 1)) = union (rng S)

proof

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
A9: ( x in y & y in rng S ) by TARSKI:def 4;
consider i being set such that
A3: ( i in dom S & y = S . i ) by A9, FUNCT_1:def 5;
A4: i in Seg (n + 1) by ASN, FINSEQ_1:def 3, A3;
reconsider i = i as Element of NAT by ASN, A3;
A5: ( 1 <= i & i <= n + 1 ) by FINSEQ_1:3, A4;

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 XBOOLE_0:def 3, A3, A9; :: thesis: verum

end;

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

then i < n + 1 by A5, XXREAL_0:1;
then i <= n by NAT_1:13;
then i in Seg n by A5;
then i in (dom S) /\ (Seg n) by A3, XBOOLE_0:def 4;
then A8: i in dom SN by RELAT_1:90;
then S . i = SN . i by FUNCT_1:70;
then y in rng SN by FUNCT_1:def 5, A3, A8;
then x in union (rng SN) by A9, 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 L1: union (rng S) c= (union (rng SN)) \/ (S . (n + 1)) by TARSKI:def 3;
(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 A3P: 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 A3P, XBOOLE_0:def 3;

suppose C1: 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 ASN, FINSEQ_1:def 3;
then S . (n + 1) in rng S by FUNCT_1:def 5;
hence x in union (rng S) by C1, 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
A9: ( x in y & y in rng SN ) by TARSKI:def 4;
consider i being set such that
A3: ( i in dom SN & y = SN . i ) by A9, FUNCT_1:def 5;
A4: i in (dom S) /\ (Seg n) by RELAT_1:90, A3;
A5: SN . i = S . i by FUNCT_1:70, A3;
i in dom S by A4, XBOOLE_0:def 4;
then y in rng S by A3, A5, FUNCT_1:def 5;
hence x in union (rng S) by A9, TARSKI:def 4; :: thesis: verum

end;

end;

end;

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

end;

hence (union (rng SN)) \/ (S . (n + 1)) = union (rng S) by L1, XBOOLE_0:def 10; :: thesis: verum

end;

AA: ( 1 <= n + 1 & n + 1 <= len L ) by ASN, NAT_1:11;
Q7P: L = (L | n) ^ <*(L /. (len L))*> by ASN, FINSEQ_5:24
.= LN ^ <*(L . (n + 1))*> by AA, ASN, FINSEQ_4:24 ;
reconsider USN = union (rng SN) as finite set by P1, Q1, Q2, Q3, Q4;
reconsider S1 = S . (n + 1) as finite set by ASN, Q0;
union (rng S) = USN \/ S1 by Q6;
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 A2: y in rng SN ; :: thesis: y misses S . (n + 1)
consider i being set such that
A3: ( i in dom SN & y = SN . i ) by A2, FUNCT_1:def 5;
A4P: i in (dom S) /\ (Seg n) by A3, RELAT_1:90;
then A4: i in Seg n by XBOOLE_0:def 4;
reconsider i = i as Element of NAT by A4P;
i <= n by FINSEQ_1:3, A4;
then A0P: i <> n + 1 by NAT_1:13;
y = S . i by A3, FUNCT_1:70;
hence y misses S . (n + 1) by A0P, PROB_2:def 3, ASN; :: thesis: verum

end;

then Q9: union (rng SN) misses S . (n + 1) by ZFMISC_1:98;
Q8: card ((union (rng SN)) \/ (S . (n + 1))) = (card USN) + (card S1) by Q9, CARD_2:53;
thus card (union (rng S)) = (Sum LN) + (L . (n + 1)) by Q5, ASN, Q0, Q8, Q6
.= Sum L by Q7P, RVSUM_1:104 ; :: thesis: verum

end;

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

end;

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