let F be non empty finite set ; :: thesis: for A being non empty FinSequence of bool F st A is Hall holds
ex G being Singlification of A st G is Hall
let A be non empty FinSequence of bool F; :: thesis: ( A is Hall implies ex G being Singlification of A st G is Hall )
assume A1:
A is Hall
; :: thesis: ex G being Singlification of A st G is Hall
then A2:
A is non-empty
by Th15;
defpred S1[ Element of NAT ] means ( $1 in dom A implies ex g being Singlification of A,$1 st
( g is Hall & ( for k being Element of NAT st 1 <= k & k <= $1 holds
g is Singlification of A,k ) ) );
A3:
S1[ 0 ]
A5:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A6:
S1[
k]
;
:: thesis: S1[k + 1]
(
k + 1
in dom A implies ex
g being
Singlification of
A,
k + 1 st
(
g is
Hall & ( for
l being
Element of
NAT st 1
<= l &
l <= k + 1 holds
g is
Singlification of
A,
l ) ) )
proof
assume A7:
k + 1
in dom A
;
:: thesis: ex g being Singlification of A,k + 1 st
( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds
g is Singlification of A,l ) )
per cases
( k = 0 or k in dom A )
by A7, TAXONOM1:1;
suppose A10:
k in dom A
;
:: thesis: ex g being Singlification of A,k + 1 st
( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds
g is Singlification of A,l ) )then consider g being
Singlification of
A,
k such that A11:
(
g is
Hall & ( for
l being
Element of
NAT st 1
<= l &
l <= k holds
g is
Singlification of
A,
l ) )
by A6;
A12:
dom g = dom A
by Def6;
k + 1
in dom g
by A7, Def6;
then consider G being
Singlification of
g,
k + 1
such that A13:
G is
Hall
by A11, Th30;
A14:
dom G = dom A
by A12, Def6;
A15:
G is
non-empty
by A13, Th15;
then A16:
G . k <> {}
by A10, A14;
g is
non-empty
by A11, Th15;
then A17:
g . (k + 1) <> {}
by A7, A12;
then reconsider G =
G as
Singlification of
A,
k + 1
by A2, A7, A10, A16, Th24;
for
l being
Element of
NAT st 1
<= l &
l <= k + 1 holds
G is
Singlification of
A,
l
hence
ex
g being
Singlification of
A,
k + 1 st
(
g is
Hall & ( for
l being
Element of
NAT st 1
<= l &
l <= k + 1 holds
g is
Singlification of
A,
l ) )
by A13;
:: thesis: verum end;
end;
hence
S1[
k + 1]
;
:: thesis: verum
end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A3, A5);
then
( len A in dom A implies ex g being Singlification of A, len A st
( g is Hall & ( for l being Element of NAT st 1 <= l & l <= len A holds
g is Singlification of A,l ) ) )
;
then consider G being Singlification of A, len A such that
A21:
( G is Hall & ( for l being Element of NAT st 1 <= l & l <= len A holds
G is Singlification of A,l ) )
by FINSEQ_5:6;
A22:
dom G = dom A
by Def6;
for i being Element of NAT st i in dom A holds
G is Singlification of A,i
then
G is Singlification of A
by A2, A22, Th27;
hence
ex G being Singlification of A st G is Hall
by A21; :: thesis: verum