let X be finite set ; :: thesis: for f being FinSequence of bool X st ( for d, e being Nat st d in dom f & e in dom f & d <> e holds

f . d misses f . e ) holds

card (union (rng f)) = Sum (Card f)

defpred S_{1}[ Nat] means for f being FinSequence of bool X st len f = $1 & ( for d, e being Nat st d in dom f & e in dom f & d <> e holds

f . d misses f . e ) holds

card (union (rng f)) = Sum (Card f);

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]

f . d misses f . e ) implies card (union (rng f)) = Sum (Card f) )

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A25, A1);

then S_{1}[ len f]
;

hence ( ( for d, e being Nat st d in dom f & e in dom f & d <> e holds

f . d misses f . e ) implies card (union (rng f)) = Sum (Card f) ) ; :: thesis: verum

f . d misses f . e ) holds

card (union (rng f)) = Sum (Card f)

defpred S

f . d misses f . e ) holds

card (union (rng f)) = Sum (Card f);

A1: for n being Nat st S

S

proof

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

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

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

end;assume A2: S

S

proof

hence
S
let f be FinSequence of bool X; :: thesis: ( len f = n + 1 & ( for d, e being Nat st d in dom f & e in dom f & d <> e holds

f . d misses f . e ) implies card (union (rng f)) = Sum (Card f) )

assume that

A3: len f = n + 1 and

A4: for d, e being Nat st d in dom f & e in dom f & d <> e holds

f . d misses f . e ; :: thesis: card (union (rng f)) = Sum (Card f)

A5: f <> {} by A3;

then consider f1 being FinSequence of bool X, Y being Element of bool X such that

A6: f = f1 ^ <*Y*> by HILBERT2:4;

reconsider F1 = union (rng f1) as finite set ;

A7: union (rng f) = union ((rng f1) \/ (rng <*Y*>)) by A6, FINSEQ_1:31

.= union ((rng f1) \/ {Y}) by FINSEQ_1:38

.= F1 \/ (union {Y}) by ZFMISC_1:78

.= F1 \/ Y by ZFMISC_1:25 ;

A8: n + 1 = (len f1) + 1 by A3, A6, FINSEQ_2:16;

F1 misses Y

reconsider gg = <*(card Y)*> as FinSequence of NAT ;

A18: Card f = (Card f1) ^ (Card <*Y*>) by A6, PRE_POLY:25

.= (Card f1) ^ gg by PRE_POLY:24 ;

for d, e being Nat st d in dom f1 & e in dom f1 & d <> e holds

f1 . d misses f1 . e

hence card (union (rng f)) = Sum (Card f) by A17, A18, A7, RVSUM_1:74; :: thesis: verum

end;f . d misses f . e ) implies card (union (rng f)) = Sum (Card f) )

assume that

A3: len f = n + 1 and

A4: for d, e being Nat st d in dom f & e in dom f & d <> e holds

f . d misses f . e ; :: thesis: card (union (rng f)) = Sum (Card f)

A5: f <> {} by A3;

then consider f1 being FinSequence of bool X, Y being Element of bool X such that

A6: f = f1 ^ <*Y*> by HILBERT2:4;

reconsider F1 = union (rng f1) as finite set ;

A7: union (rng f) = union ((rng f1) \/ (rng <*Y*>)) by A6, FINSEQ_1:31

.= union ((rng f1) \/ {Y}) by FINSEQ_1:38

.= F1 \/ (union {Y}) by ZFMISC_1:78

.= F1 \/ Y by ZFMISC_1:25 ;

A8: n + 1 = (len f1) + 1 by A3, A6, FINSEQ_2:16;

F1 misses Y

proof

then A17:
(card F1) + (card Y) = card (F1 \/ Y)
by CARD_2:40;
A9:
n + 1 in dom f
by A3, A5, FINSEQ_5:6;

assume F1 meets Y ; :: thesis: contradiction

then consider x being object such that

A10: x in F1 /\ Y by XBOOLE_0:4;

x in F1 by A10, XBOOLE_0:def 4;

then consider Z being set such that

A11: x in Z and

A12: Z in rng f1 by TARSKI:def 4;

consider k being Nat such that

A13: k in dom f1 and

A14: f1 . k = Z by A12, FINSEQ_2:10;

k <= n by A8, A13, FINSEQ_3:25;

then A15: k < n + 1 by NAT_1:13;

k in dom f by A6, A13, FINSEQ_2:15;

then f . (n + 1) misses f . k by A4, A15, A9;

then Y misses f . k by A6, A8, FINSEQ_1:42;

then A16: Y misses Z by A6, A13, A14, FINSEQ_1:def 7;

x in Y \/ Z by A11, XBOOLE_0:def 3;

then not x in Y by A11, A16, XBOOLE_0:5;

hence contradiction by A10, XBOOLE_0:def 4; :: thesis: verum

end;assume F1 meets Y ; :: thesis: contradiction

then consider x being object such that

A10: x in F1 /\ Y by XBOOLE_0:4;

x in F1 by A10, XBOOLE_0:def 4;

then consider Z being set such that

A11: x in Z and

A12: Z in rng f1 by TARSKI:def 4;

consider k being Nat such that

A13: k in dom f1 and

A14: f1 . k = Z by A12, FINSEQ_2:10;

k <= n by A8, A13, FINSEQ_3:25;

then A15: k < n + 1 by NAT_1:13;

k in dom f by A6, A13, FINSEQ_2:15;

then f . (n + 1) misses f . k by A4, A15, A9;

then Y misses f . k by A6, A8, FINSEQ_1:42;

then A16: Y misses Z by A6, A13, A14, FINSEQ_1:def 7;

x in Y \/ Z by A11, XBOOLE_0:def 3;

then not x in Y by A11, A16, XBOOLE_0:5;

hence contradiction by A10, XBOOLE_0:def 4; :: thesis: verum

reconsider gg = <*(card Y)*> as FinSequence of NAT ;

A18: Card f = (Card f1) ^ (Card <*Y*>) by A6, PRE_POLY:25

.= (Card f1) ^ gg by PRE_POLY:24 ;

for d, e being Nat st d in dom f1 & e in dom f1 & d <> e holds

f1 . d misses f1 . e

proof

then
card (union (rng f1)) = Sum (Card f1)
by A2, A8;
let d, e be Nat; :: thesis: ( d in dom f1 & e in dom f1 & d <> e implies f1 . d misses f1 . e )

assume that

A19: d in dom f1 and

A20: e in dom f1 and

A21: d <> e ; :: thesis: f1 . d misses f1 . e

A22: f . e = f1 . e by A6, A20, FINSEQ_1:def 7;

A23: e in dom f by A6, A20, FINSEQ_2:15;

A24: d in dom f by A6, A19, FINSEQ_2:15;

f . d = f1 . d by A6, A19, FINSEQ_1:def 7;

hence f1 . d misses f1 . e by A4, A21, A22, A24, A23; :: thesis: verum

end;assume that

A19: d in dom f1 and

A20: e in dom f1 and

A21: d <> e ; :: thesis: f1 . d misses f1 . e

A22: f . e = f1 . e by A6, A20, FINSEQ_1:def 7;

A23: e in dom f by A6, A20, FINSEQ_2:15;

A24: d in dom f by A6, A19, FINSEQ_2:15;

f . d = f1 . d by A6, A19, FINSEQ_1:def 7;

hence f1 . d misses f1 . e by A4, A21, A22, A24, A23; :: thesis: verum

hence card (union (rng f)) = Sum (Card f) by A17, A18, A7, RVSUM_1:74; :: thesis: verum

proof

let f be FinSequence of bool X; :: thesis: ( ( for d, e being Nat st d in dom f & e in dom f & d <> e holds
let f be FinSequence of bool X; :: thesis: ( len f = 0 & ( for d, e being Nat st d in dom f & e in dom f & d <> e holds

f . d misses f . e ) implies card (union (rng f)) = Sum (Card f) )

assume that

A26: len f = 0 and

for d, e being Nat st d in dom f & e in dom f & d <> e holds

f . d misses f . e ; :: thesis: card (union (rng f)) = Sum (Card f)

A27: Card {} = {} ;

f = {} by A26;

hence card (union (rng f)) = Sum (Card f) by A27, CARD_1:27, RVSUM_1:72, ZFMISC_1:2; :: thesis: verum

end;f . d misses f . e ) implies card (union (rng f)) = Sum (Card f) )

assume that

A26: len f = 0 and

for d, e being Nat st d in dom f & e in dom f & d <> e holds

f . d misses f . e ; :: thesis: card (union (rng f)) = Sum (Card f)

A27: Card {} = {} ;

f = {} by A26;

hence card (union (rng f)) = Sum (Card f) by A27, CARD_1:27, RVSUM_1:72, ZFMISC_1:2; :: thesis: verum

f . d misses f . e ) implies card (union (rng f)) = Sum (Card f) )

for n being Nat holds S

then S

hence ( ( for d, e being Nat st d in dom f & e in dom f & d <> e holds

f . d misses f . e ) implies card (union (rng f)) = Sum (Card f) ) ; :: thesis: verum