let F be finite set ; for A being FinSequence of bool F
for i being Element of NAT st i in dom A & A is Hall holds
ex G being Singlification of A,i st G is Hall
let A be FinSequence of bool F; for i being Element of NAT st i in dom A & A is Hall holds
ex G being Singlification of A,i st G is Hall
let i be Element of NAT ; ( i in dom A & A is Hall implies ex G being Singlification of A,i st G is Hall )
assume that
A1:
i in dom A
and
A2:
A is Hall
; ex G being Singlification of A,i st G is Hall
A3:
A . i <> {}
by A1, A2, Th16, CARD_1:27;
set n = card (A . i);
A4:
card (A . i) >= 1
by A1, A2, Th16;
defpred S1[ Element of NAT ] means ex G being Reduction of A st
( G is Hall & card (G . i) = $1 );
A5:
A is Reduction of A
by Th26;
per cases
( card (A . i) = 1 or card (A . i) > 1 )
by A4, XXREAL_0:1;
suppose A6:
card (A . i) > 1
;
ex G being Singlification of A,i st G is Hall A7:
for
k being
Element of
NAT st
k >= 1 &
S1[
k + 1] holds
S1[
k]
proof
let k be
Element of
NAT ;
( k >= 1 & S1[k + 1] implies S1[k] )
assume that A8:
k >= 1
and A9:
S1[
k + 1]
;
S1[k]
consider G being
Reduction of
A such that A10:
G is
Hall
and A11:
card (G . i) = k + 1
by A9;
1
+ 1
<= k + 1
by A8, XREAL_1:6;
then consider x being
set such that A12:
x in G . i
and A13:
Cut (
G,
i,
x) is
Hall
by A10, A11, Th29;
set H =
Cut (
G,
i,
x);
A14:
dom G = dom A
by Def6;
then
Cut (
G,
i,
x) is
Reduction of
G
by A1, Th21;
then A15:
Cut (
G,
i,
x) is
Reduction of
A
by Th22;
card ((Cut (G,i,x)) . i) =
(k + 1) - 1
by A1, A11, A14, A12, Th11
.=
k
;
hence
S1[
k]
by A13, A15;
verum
end;
A is
Reduction of
A
by Th26;
then A16:
ex
n being
Element of
NAT st
(
n > 1 &
S1[
n] )
by A2, A6;
S1[1]
from HALLMAR1:sch 2(A16, A7);
then consider G being
Reduction of
A such that A17:
G is
Hall
and A18:
card (G . i) = 1
;
G is
Singlification of
A,
i
by A1, A3, A18, Def7;
hence
ex
G being
Singlification of
A,
i st
G is
Hall
by A17;
verum end;