reconsider F = F as Function of ((bool (the_universe_of (X \/ NAT))) ^omega),(bool (the_universe_of (X \/ NAT))) by a1, A11, FUNCT_2:3;
deffunc H₁( XFinSequence of ) -> Element of bool (the_universe_of (X \/ NAT)) = F . $1;
consider f being Function of NAT,(bool (the_universe_of (X \/ NAT))) such that
A43: for n being natural number holds f . n = H₁(f | n) from ALGSTR_4:sch 4();
take f ; :: thesis: ( f . 0 = {} & f . 1 = X & ( for n being natural number st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(f . p),(f . (n - p)):] ) & f . n = Union (disjoin fs) ) ) )
A44: {} in (bool (the_universe_of (X \/ NAT))) ^omega by AFINSQ_1:43;
A45: dom {} = {} ;
thus f . 0 = F . (f | 0) by A43
.= {} by A44, A45, A11 ; :: thesis: ( f . 1 = X & ( for n being natural number st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(f . p),(f . (n - p)):] ) & f . n = Union (disjoin fs) ) ) )
1 c= NAT ;
then 1 c= dom f by FUNCT_2:def 1;
then A46: dom (f | 1) = 1 by RELAT_1:62;
A47: f | 1 in (bool (the_universe_of (X \/ NAT))) ^omega by AFINSQ_1:42;
thus f . 1 = F . (f | 1) by A43
.= X by A46, A47, A11 ; :: thesis: for n being natural number st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(f . p),(f . (n - p)):] ) & f . n = Union (disjoin fs) )
let n be natural number ; :: thesis: ( n >= 2 implies ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(f . p),(f . (n - p)):] ) & f . n = Union (disjoin fs) ) )
assume A48: n >= 2 ; :: thesis: ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(f . p),(f . (n - p)):] ) & f . n = Union (disjoin fs) )
n c= NAT ;
then n c= dom f by FUNCT_2:def 1;
then A49: dom (f | n) = n by RELAT_1:62;
f | n in (bool (the_universe_of (X \/ NAT))) ^omega by AFINSQ_1:42;
then consider fs1 being FinSequence such that
A50: ( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs1 . p = [:((f | n) . p),((f | n) . (n - p)):] ) & F . (f | n) = Union (disjoin fs1) ) by A48, A49, A11;
take fs1 ; :: thesis: ( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs1 . p = [:(f . p),(f . (n - p)):] ) & f . n = Union (disjoin fs1) )
thus len fs1 = n - 1 by A50; :: thesis: ( ( for p being natural number st p >= 1 & p <= n - 1 holds
fs1 . p = [:(f . p),(f . (n - p)):] ) & f . n = Union (disjoin fs1) )
thus for p being natural number st p >= 1 & p <= n - 1 holds
fs1 . p = [:(f . p),(f . (n - p)):] :: thesis: f . n = Union (disjoin fs1)

proof

let p be natural number ; :: thesis: ( p >= 1 & p <= n - 1 implies fs1 . p = [:(f . p),(f . (n - p)):] )
assume A51: ( p >= 1 & p <= n - 1 ) ; :: thesis: fs1 . p = [:(f . p),(f . (n - p)):]
set n9 = n -' 1;
n - 1 >= 2 - 1 by A48, XREAL_1:9;
then A52: n -' 1 = n - 1 by XREAL_0:def 2;
then A53: p in Seg (n -' 1) by A51, FINSEQ_1:1;
Seg (n -' 1) c= (n -' 1) + 1 by AFINSQ_1:3;
then A54: (f | n) . p = f . p by A52, A53, FUNCT_1:49;
( - p <= - 1 & - p >= - (n - 1) ) by A51, XREAL_1:24;
then A55: ( (- p) + n <= (- 1) + n & (- p) + n >= (- (n - 1)) + n ) by XREAL_1:6;
then A56: ( n - p <= n -' 1 & n - p >= 1 ) by XREAL_0:def 2;
A57: n - p = n -' p by A55, XREAL_0:def 2;
then A58: n -' p in Seg (n -' 1) by A56, FINSEQ_1:1;
A59: Seg (n -' 1) c= (n -' 1) + 1 by AFINSQ_1:3;
thus fs1 . p = [:((f | n) . p),((f | n) . (n - p)):] by A51, A50
.= [:(f . p),(f . (n - p)):] by A54, A59, A57, A52, A58, FUNCT_1:49 ; :: thesis: verum

end;

thus f . n = Union (disjoin fs1) by A50, A43; :: thesis: verum