defpred S_{1}[ 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 );

_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A41, A1); :: thesis: verum

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_{1}[n] holds

S_{1}[n + 1]

A41:
SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[n + 1]

_{1}[n + 1]
; :: thesis: verum

end;assume A2: S

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 )

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

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

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

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)

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

then A16:
Union S c= (Union (S | (Seg n))) \/ (S . (n + 1))
;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;

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

hence
x in (Union (S | (Seg n))) \/ (S . (n + 1))
; :: thesis: verumper cases
( i = n + 1 or i <> n + 1 )
;

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

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

proof

then A25:
(Union (S | (Seg n))) \/ (S . (n + 1)) = Union S
by A16;
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

end;assume A18: x in (Union (S | (Seg n))) \/ (S . (n + 1)) ; :: thesis: x in Union S

now :: thesis: x in Union Send;

hence
x in Union S
; :: thesis: verumper cases
( x in S . (n + 1) or x in Union (S | (Seg n)) )
by A18, XBOOLE_0:def 3;

end;

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

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

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

A30:
S | (Seg n) is disjoint_valued
by Lm1, A3;
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;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

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

then
Union (S | (Seg n)) misses S . (n + 1)
by ZFMISC_1:80;
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;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

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

proof

thus
for n being Nat holds S
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;( 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