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:47;
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:91;
A47: f | 1 in (bool (the_universe_of (X \/ NAT ))) ^omega by AFINSQ_1:46;
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:91;
A50: f | n in (bool (the_universe_of (X \/ NAT ))) ^omega by AFINSQ_1:46;
consider fs1 being FinSequence such that
A51: ( 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, A50, 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 A51; :: 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 A52: ( 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:11;
then A53: n -' 1 = n - 1 by XREAL_0:def 2;
then A54: p in Seg (n -' 1) by A52, FINSEQ_1:3;
Seg (n -' 1) c= (n -' 1) + 1 by AFINSQ_1:5;
then A55: (f | n) . p = f . p by A53, A54, FUNCT_1:72;
( - p <= - 1 & - p >= - (n - 1) ) by A52, XREAL_1:26;
then A56: ( (- p) + n <= (- 1) + n & (- p) + n >= (- (n - 1)) + n ) by XREAL_1:8;
then A57: ( n - p <= n -' 1 & n - p >= 1 ) by XREAL_0:def 2;
A58: n - p = n -' p by A56, XREAL_0:def 2;
then A59: n -' p in Seg (n -' 1) by A57, FINSEQ_1:3;
A60: Seg (n -' 1) c= (n -' 1) + 1 by AFINSQ_1:5;
thus fs1 . p = [:((f | n) . p),((f | n) . (n - p)):] by A52, A51
.= [:(f . p),(f . (n - p)):] by A55, A60, A58, A53, A59, FUNCT_1:72 ; :: thesis: verum

end;

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