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 :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

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

now :: thesis: for S being Function
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 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 )
set SN = S | (Seg n);
reconsider LN = L | n as FinSequence of NAT ;
A7: n = len LN by A5, FINSEQ_1:59, NAT_1:12;

now :: thesis: for x being object st x in Union S holds
x in (Union (S | (Seg n))) \/ (S . (n + 1))

let x be object ; :: thesis: ( x in Union S implies x in (Union (S | (Seg n))) \/ (S . (n + 1)) )
assume x in Union S ; :: thesis: x in (Union (S | (Seg n))) \/ (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 object 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 :: thesis: x in (Union (S | (Seg n))) \/ (S . (n + 1))

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

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

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

end;

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

end;

end;

end;

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

end;

then A16: Union S c= (Union (S | (Seg n))) \/ (S . (n + 1)) ;
A17: (Union (S | (Seg n))) \/ (S . (n + 1)) c= Union S

proof

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

now :: thesis: x in Union S

per cases ( x in S . (n + 1) or x in Union (S | (Seg n)) ) 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 (S | (Seg n)) ; :: thesis: x in Union S

then consider y being set such that
A20: x in y and
A21: y in rng (S | (Seg n)) by TARSKI:def 4;
consider i being object such that
A22: i in dom (S | (Seg n)) and
A23: y = (S | (Seg n)) . 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;
(S | (Seg n)) . 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 (S | (Seg n))) \/ (S . (n + 1)) = Union S by A16;
A26: for i being Nat st i in dom (S | (Seg n)) holds
( (S | (Seg n)) . i is finite & LN . i = card ((S | (Seg n)) . i) )

proof

let i be Nat; :: thesis: ( i in dom (S | (Seg n)) implies ( (S | (Seg n)) . i is finite & LN . i = card ((S | (Seg n)) . i) ) )
assume A27: i in dom (S | (Seg n)) ; :: thesis: ( (S | (Seg n)) . i is finite & LN . i = card ((S | (Seg n)) . 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 ((S | (Seg n)) . i) by A27, FUNCT_1:47 ;
hence ( (S | (Seg n)) . i is finite & LN . i = card ((S | (Seg n)) . i) ) ; :: thesis: verum

end;

A30: S | (Seg n) is disjoint_valued by Lm1, A3;
A31: dom (S | (Seg n)) = (dom S) /\ (Seg n) by RELAT_1:61
.= dom LN by A4, RELAT_1:61 ;
then A32: card (Union (S | (Seg n))) = Sum LN by A2, A30, A7, A26;
reconsider USN = Union (S | (Seg n)) as finite set by A2, A30, A31, A7, A26;
A33: 1 <= n + 1 by NAT_1:11;
A34: L = (L | n) ^ <*(L /. (len L))*> by A5, FINSEQ_5:21
.= LN ^ <*(L . (n + 1))*> by A5, A33, FINSEQ_4:15 ;
n + 1 in Seg (len L) by A5, FINSEQ_1:4;
then A35: 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;
hence Union S is finite ; :: thesis: card (Union S) = Sum L
for z being set st z in rng (S | (Seg n)) holds
z misses S . (n + 1)

proof

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

end;

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

end;

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

end;

A41: 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
A42: dom S = dom L and
A43: 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 )
A44: L = {} by A43;
then S = {} by A42;
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 A44, RVSUM_1:72; :: thesis: verum

end;

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