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₁[ 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₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: 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 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

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;

then A17: (card F1) + (card Y) = card (F1 \/ Y) by CARD_2:40;
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

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;

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

end;

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

end;

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

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
f . d misses f . e ) implies card (union (rng f)) = Sum (Card f) )
for n being Nat holds S₁[n] from NAT_1:sch 2(A25, A1);
then S₁[ 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