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 )
defpred S₁[ 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 ) ) );
assume A1: A is Hall ; :: thesis: ex G being Singlification of A st G is Hall
then A2: A is non-empty ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[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 A5: 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 A5, TAXONOM1:1;

suppose A6: k = 0 ; :: 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 ) )

consider g being Singlification of A,k + 1 such that
A7: g is Hall by A1, A5, Th30;
for l being Element of NAT st 1 <= l & l <= k + 1 holds
g is Singlification of A,l by A6, XXREAL_0:1;
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 A7; :: thesis: verum

end;

suppose A8: 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
A9: g is Hall and
A10: for l being Element of NAT st 1 <= l & l <= k holds
g is Singlification of A,l by A4;
k + 1 in dom g by A5, Def6;
then consider G being Singlification of g,k + 1 such that
A11: G is Hall by A9, Th30;
A12: dom g = dom A by Def6;
then A13: dom G = dom A by Def6;
then A14: G . k <> {} by A8, A11;
k in NAT by ORDINAL1:def 12;
then A15: g . (k + 1) <> {} by A9, A5, A12;
then reconsider G = G as Singlification of A,k + 1 by A2, A5, A8, A14, Th24;
for l being Element of NAT st 1 <= l & l <= k + 1 holds
G is Singlification of A,l

proof

let l be Element of NAT ; :: thesis: ( 1 <= l & l <= k + 1 implies G is Singlification of A,l )
assume that
A16: 1 <= l and
A17: l <= k + 1 ; :: thesis: G is Singlification of A,l
k + 1 <= len A by A5, FINSEQ_3:25;
then l <= len A by A17, XXREAL_0:2;
then A18: l in dom A by A16, FINSEQ_3:25;
then A19: G . l <> {} by A13, A11;

per cases ( l <= k or l = k + 1 ) by A17, NAT_1:8;

suppose l <= k ; :: thesis: G is Singlification of A,l

then g is Singlification of A,l by A10, A16;
hence G is Singlification of A,l by A2, A5, A15, A18, A19, Th24; :: thesis: verum

end;

suppose l = k + 1 ; :: thesis: G is Singlification of A,l

hence G is Singlification of A,l ; :: thesis: verum

end;

end;

end;

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 A11; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A20: S₁[ 0 ]

proof

assume 0 in dom A ; :: thesis: ex g being Singlification of A, 0 st
( g is Hall & ( for k being Element of NAT st 1 <= k & k <= 0 holds
g is Singlification of A,k ) )
then consider G being Singlification of A, 0 such that
A21: G is Hall by A1, Th30;
for k being Element of NAT st 1 <= k & k <= 0 holds
G is Singlification of A,k ;
hence ex g being Singlification of A, 0 st
( g is Hall & ( for k being Element of NAT st 1 <= k & k <= 0 holds
g is Singlification of A,k ) ) by A21; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A20, A3);
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
A22: G is Hall and
A23: for l being Element of NAT st 1 <= l & l <= len A holds
G is Singlification of A,l by FINSEQ_5:6;
A24: for i being Element of NAT st i in dom A holds
G is Singlification of A,i

proof

let i be Element of NAT ; :: thesis: ( i in dom A implies G is Singlification of A,i )
assume i in dom A ; :: thesis: G is Singlification of A,i
then ( 1 <= i & i <= len A ) by FINSEQ_3:25;
hence G is Singlification of A,i by A23; :: thesis: verum

end;

dom G = dom A by Def6;
then G is Singlification of A by A2, A24, Th27;
hence ex G being Singlification of A st G is Hall by A22; :: thesis: verum