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