let n be Nat; :: thesis: for X being finite set
for f being FinSequence of bool X st len f = n & ( 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)
let X be finite set ; :: thesis: for f being FinSequence of bool X st len f = n & ( 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₁[ 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: S₁[ 0 ]

proof

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 ( 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 ) ) ; :: thesis: card (union (rng f)) = Sum (Card f)
then f = {} ;
hence card (union (rng f)) = Sum (Card f) by CARD_1:47, CARD_3:9, RVSUM_1:102, ZFMISC_1:2; :: thesis: verum

end;

A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
S₁[n + 1]

proof

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 A4: ( 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 ) ) ; :: thesis: card (union (rng f)) = Sum (Card f)
then A5: f <> {} ;
then consider f1 being FinSequence of bool X, Y being Element of bool X such that
A6: f = f1 ^ <*Y*> by HILBERT2:4;
A7: n + 1 = (len f1) + 1 by A4, A6, FINSEQ_2:19;
for d, e being Nat st d in dom f1 & e in dom f1 & d <> e holds
f1 . d misses f1 . e

proof

let d, e be Nat; :: thesis: ( d in dom f1 & e in dom f1 & d <> e implies f1 . d misses f1 . e )
assume A8: ( d in dom f1 & e in dom f1 & d <> e ) ; :: thesis: f1 . d misses f1 . e
then A9: ( f . d = f1 . d & f . e = f1 . e ) by A6, FINSEQ_1:def 7;
( d in dom f & e in dom f ) by A6, A8, FINSEQ_2:18;
hence f1 . d misses f1 . e by A4, A8, A9; :: thesis: verum

end;

then A10: card (union (rng f1)) = Sum (Card f1) by A3, A7;
Union f1 is finite ;
then reconsider F1 = union (rng f1) as finite set ;
F1 misses Y

proof

assume F1 meets Y ; :: thesis: contradiction
then consider x being set such that
A11: x in F1 /\ Y by XBOOLE_0:4;
x in F1 by A11, XBOOLE_0:def 4;
then consider Z being set such that
A12: ( x in Z & Z in rng f1 ) by TARSKI:def 4;
consider k being Nat such that
A13: ( k in dom f1 & f1 . k = Z ) by A12, FINSEQ_2:11;
k <= n by A7, A13, FINSEQ_3:27;
then A14: k < n + 1 by NAT_1:13;
A15: n + 1 in dom f by A4, A5, FINSEQ_5:6;
k in dom f by A6, A13, FINSEQ_2:18;
then f . (n + 1) misses f . k by A4, A14, A15;
then Y misses f . k by A6, A7, FINSEQ_1:59;
then A16: Y misses Z by A6, A13, FINSEQ_1:def 7;
x in Y \/ Z by A12, XBOOLE_0:def 3;
then not x in Y by A12, A16, XBOOLE_0:5;
hence contradiction by A11, XBOOLE_0:def 4; :: thesis: verum

end;

then A17: (card F1) + (card Y) = card (F1 \/ Y) by CARD_2:53;
reconsider gg = <*(card Y)*> as FinSequence of NAT ;
A18: Card f = (Card f1) ^ (Card <*Y*>) by A6, POLYNOM1:13
.= (Card f1) ^ gg by POLYNOM1:12 ;
union (rng f) = union ((rng f1) \/ (rng <*Y*>)) by A6, FINSEQ_1:44
.= union ((rng f1) \/ {Y}) by FINSEQ_1:55
.= F1 \/ (union {Y}) by ZFMISC_1:96
.= F1 \/ Y by ZFMISC_1:31 ;
hence card (union (rng f)) = Sum (Card f) by A10, A17, A18, RVSUM_1:104; :: thesis: verum
thus verum ; :: thesis: verum

end;

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

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence for f being FinSequence of bool X st len f = n & ( 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) ; :: thesis: verum