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 S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
S1[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) \/ ()) by
.= union ((rng f1) \/ {Y}) by FINSEQ_1:38
.= F1 \/ () by ZFMISC_1:78
.= F1 \/ Y by ZFMISC_1:25 ;
A8: n + 1 = (len f1) + 1 by ;
F1 misses Y
proof
A9: n + 1 in dom f by ;
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 ;
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 ;
k <= n by ;
then A15: k < n + 1 by NAT_1:13;
k in dom f by ;
then f . (n + 1) misses f . k by A4, A15, A9;
then Y misses f . k by ;
then A16: Y misses Z by ;
x in Y \/ Z by ;
then not x in Y by ;
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) ^ () by
.= (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 ;
A23: e in dom f by ;
A24: d in dom f by ;
f . d = f1 . d by ;
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 ; :: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
A25: S1[ 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 ; :: 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 S1[n] from NAT_1:sch 2(A25, A1);
then S1[ 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