let X be finite set ; 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;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
S1[
n + 1]
proof
let f be
FinSequence of
bool X;
( 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
;
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
;
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;
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;
( 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
;
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;
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;
verum
end;
hence
S1[
n + 1]
;
verum
end;
A25:
S1[ 0 ]
let f be FinSequence of bool X; ( ( 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) )
; verum