let F be finite set ; for A being FinSequence of bool F st ex X being set st X is_a_system_of_different_representatives_of A holds
A is Hall
let A be FinSequence of bool F; ( ex X being set st X is_a_system_of_different_representatives_of A implies A is Hall )
given X being set such that A1:
X is_a_system_of_different_representatives_of A
; A is Hall
consider f being FinSequence of F such that
f = X
and
A2:
dom A = dom f
and
A3:
for i being Element of NAT st i in dom f holds
f . i in A . i
and
A4:
f is one-to-one
by A1;
for J being finite set st J c= dom A holds
card J <= card (union (A,J))
proof
let J be
finite set ;
( J c= dom A implies card J <= card (union (A,J)) )
set X =
J;
set Y =
union (
A,
J);
set g =
f | J;
assume A5:
J c= dom A
;
card J <= card (union (A,J))
then A6:
dom (f | J) = J
by A2, RELAT_1:62;
A7:
dom (f | J) c= dom f
by RELAT_1:60;
A8:
rng (f | J) c= union (
A,
J)
proof
let x be
object ;
TARSKI:def 3 ( not x in rng (f | J) or x in union (A,J) )
assume
x in rng (f | J)
;
x in union (A,J)
then consider a being
object such that A9:
a in dom (f | J)
and A10:
x = (f | J) . a
by FUNCT_1:def 3;
a in dom f
by A7, A9;
then reconsider a =
a as
Element of
NAT ;
f . a in A . a
by A2, A3, A5, A6, A9;
then
(f | J) . a in A . a
by A9, FUNCT_1:47;
hence
x in union (
A,
J)
by A5, A6, A9, A10, Def1;
verum
end;
f | J is
one-to-one
by A4, FUNCT_1:52;
then
Segm (card J) c= Segm (card (union (A,J)))
by A6, A8, CARD_1:10;
hence
card J <= card (union (A,J))
by NAT_1:39;
verum
end;
hence
A is Hall
; verum