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

proof

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

end;

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