defpred S1[ 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 () = Sum L );
A1: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[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 () = 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 () = 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 () = 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 () = Sum L )
set SN = S | (Seg n);
reconsider LN = L | n as FinSequence of NAT ;
A7: n = len LN by ;
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 ;
A12: i in Seg (n + 1) by ;
reconsider i = i as Element of NAT by ;
A13: i <= n + 1 by ;
A14: 1 <= i by ;
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 ; :: thesis: verum
end;
suppose i <> n + 1 ; :: thesis: x in (Union (S | (Seg n))) \/ (S . (n + 1))
then i < n + 1 by ;
then i <= n by NAT_1:13;
then i in Seg n by A14;
then i in (dom S) /\ (Seg n) by ;
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 ;
then x in Union (S | (Seg n)) by ;
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 ;
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 ;
then S . (n + 1) in rng S by FUNCT_1:def 3;
hence x in Union S by ; :: 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 ;
i in (dom S) /\ (Seg n) by ;
then A24: i in dom S by XBOOLE_0:def 4;
(S | (Seg n)) . i = S . i by ;
then y in rng S by ;
hence x in Union S by ; :: 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
.= card (S . i) by
.= card ((S | (Seg n)) . i) by ;
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 ;
A31: dom (S | (Seg n)) = (dom S) /\ (Seg n) by RELAT_1:61
.= dom LN by ;
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
.= LN ^ <*(L . (n + 1))*> by ;
n + 1 in Seg (len L) by ;
then A35: n + 1 in dom S by ;
then reconsider S1 = S . (n + 1) as finite set by A6;
Union S = USN \/ S1 by ;
hence Union S is finite ; :: thesis: card () = 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 ;
then A39: i in Seg n by XBOOLE_0:def 4;
reconsider i = i as Element of NAT by A38;
i <= n by ;
then A40: i <> n + 1 by NAT_1:13;
y = S . i by ;
hence y misses S . (n + 1) by ; :: 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 () = (Sum LN) + (L . (n + 1)) by A6, A35, A32, A25
.= Sum L by ;
:: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
A41: S1[ 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 () = 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 () = 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 () = 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 () = Sum L ) by ; :: thesis: verum
end;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A41, A1); :: thesis: verum