let f1, f2 be sequence of (bool (the_universe_of (X \/ NAT))); :: thesis: ( f1 . 0 = {} & f1 . 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 = [:(f1 . p),(f1 . (n - p)):] ) & f1 . n = Union (disjoin fs) ) ) & f2 . 0 = {} & f2 . 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 = [:(f2 . p),(f2 . (n - p)):] ) & f2 . n = Union (disjoin fs) ) ) implies f1 = f2 )
assume A59: f1 . 0 = {} ; :: thesis: ( not f1 . 1 = X or ex n being Nat st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being Nat st
( p >= 1 & p <= n - 1 & not fs . p = [:(f1 . p),(f1 . (n - p)):] ) or not f1 . n = Union (disjoin fs) ) ) ) or not f2 . 0 = {} or not f2 . 1 = X or ex n being Nat st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being Nat st
( p >= 1 & p <= n - 1 & not fs . p = [:(f2 . p),(f2 . (n - p)):] ) or not f2 . n = Union (disjoin fs) ) ) ) or f1 = f2 )
assume A60: f1 . 1 = X ; :: thesis: ( ex n being Nat st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being Nat st
( p >= 1 & p <= n - 1 & not fs . p = [:(f1 . p),(f1 . (n - p)):] ) or not f1 . n = Union (disjoin fs) ) ) ) or not f2 . 0 = {} or not f2 . 1 = X or ex n being Nat st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being Nat st
( p >= 1 & p <= n - 1 & not fs . p = [:(f2 . p),(f2 . (n - p)):] ) or not f2 . n = Union (disjoin fs) ) ) ) or f1 = f2 )
assume A61: 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 = [:(f1 . p),(f1 . (n - p)):] ) & f1 . n = Union (disjoin fs) ) ; :: thesis: ( not f2 . 0 = {} or not f2 . 1 = X or ex n being Nat st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being Nat st
( p >= 1 & p <= n - 1 & not fs . p = [:(f2 . p),(f2 . (n - p)):] ) or not f2 . n = Union (disjoin fs) ) ) ) or f1 = f2 )
assume A62: f2 . 0 = {} ; :: thesis: ( not f2 . 1 = X or ex n being Nat st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being Nat st
( p >= 1 & p <= n - 1 & not fs . p = [:(f2 . p),(f2 . (n - p)):] ) or not f2 . n = Union (disjoin fs) ) ) ) or f1 = f2 )
assume A63: f2 . 1 = X ; :: thesis: ( ex n being Nat st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being Nat st
( p >= 1 & p <= n - 1 & not fs . p = [:(f2 . p),(f2 . (n - p)):] ) or not f2 . n = Union (disjoin fs) ) ) ) or f1 = f2 )
assume A64: 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 = [:(f2 . p),(f2 . (n - p)):] ) & f2 . n = Union (disjoin fs) ) ; :: thesis: f1 = f2
{} in (bool (the_universe_of (X \/ NAT))) ^omega by AFINSQ_1:43;
then A65: ( S₁[ {} ,F . {}] & {} is XFinSequence of bool (the_universe_of (X \/ NAT)) ) by A10, AFINSQ_1:42;
A66: dom {} = {} ;
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;
A67: for n being Nat holds f1 . n = H₁(f1 | n)

proof

let n be Nat; :: thesis: f1 . n = H₁(f1 | n)
( n = 0 or n + 1 > 0 + 1 ) by XREAL_1:6;
then ( n = 0 or n >= 1 ) by NAT_1:13;
then ( n = 0 or n = 1 or n > 1 ) by XXREAL_0:1;
then A68: ( n = 0 or n = 1 or n + 1 > 1 + 1 ) by XREAL_1:6;

per cases ( n = 0 or n = 1 or n >= 2 ) by A68, NAT_1:13;

suppose A69: n = 0 ; :: thesis: f1 . n = H₁(f1 | n)

hence f1 . n = F . {} by A65, A66, A59
.= H₁(f1 | n) by A69 ;
:: thesis: verum

end;

suppose A70: n = 1 ; :: thesis: f1 . n = H₁(f1 | n)

1 c= NAT ;
then 1 c= dom f1 by FUNCT_2:def 1;
then A71: dom (f1 | 1) = 1 by RELAT_1:62;
f1 | 1 in (bool (the_universe_of (X \/ NAT))) ^omega by AFINSQ_1:42;
hence f1 . n = H₁(f1 | n) by A70, A71, A10, A60; :: thesis: verum

end;

suppose A72: n >= 2 ; :: thesis: f1 . n = H₁(f1 | n)

n c= NAT ;
then n c= dom f1 by FUNCT_2:def 1;
then A73: dom (f1 | n) = n by RELAT_1:62;
f1 | n in (bool (the_universe_of (X \/ NAT))) ^omega by AFINSQ_1:42;
then consider fs1 being FinSequence such that
A74: ( len fs1 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs1 . p = [:((f1 | n) . p),((f1 | n) . (n - p)):] ) & F . (f1 | n) = Union (disjoin fs1) ) by A72, A73, A10;
consider fs2 being FinSequence such that
A75: ( len fs2 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs2 . p = [:(f1 . p),(f1 . (n - p)):] ) & f1 . n = Union (disjoin fs2) ) by A72, A61;
for p being Nat st 1 <= p & p <= len fs1 holds
fs1 . p = fs2 . p

proof

let p be Nat; :: thesis: ( 1 <= p & p <= len fs1 implies fs1 . p = fs2 . p )
assume A76: ( 1 <= p & p <= len fs1 ) ; :: thesis: fs1 . p = fs2 . p
then A77: fs1 . p = [:((f1 | n) . p),((f1 | n) . (n - p)):] by A74;
A78: fs2 . p = [:(f1 . p),(f1 . (n - p)):] by A76, A74, A75;
set n9 = n -' 1;
n - 1 >= 2 - 1 by A72, XREAL_1:9;
then A79: n -' 1 = n - 1 by XREAL_0:def 2;
then A80: p in Seg (n -' 1) by A76, A74, FINSEQ_1:1;
A81: Seg (n -' 1) c= Segm ((n -' 1) + 1) by AFINSQ_1:3;
( - p <= - 1 & - p >= - (n - 1) ) by A76, A74, XREAL_1:24;
then A82: ( (- p) + n <= (- 1) + n & (- p) + n >= (- (n - 1)) + n ) by XREAL_1:6;
then A83: ( n - p <= n -' 1 & n - p >= 1 ) by XREAL_0:def 2;
A84: n - p = n -' p by A82, XREAL_0:def 2;
then A85: n -' p in Seg (n -' 1) by A83, FINSEQ_1:1;
Seg (n -' 1) c= Segm ((n -' 1) + 1) by AFINSQ_1:3;
then (f1 | n) . (n - p) = f1 . (n - p) by A84, A79, A85, FUNCT_1:49;
hence fs1 . p = fs2 . p by A81, A77, A78, A79, A80, FUNCT_1:49; :: thesis: verum

end;

hence f1 . n = H₁(f1 | n) by A74, A75, FINSEQ_1:14; :: thesis: verum

end;

end;

end;

A86: for n being Nat holds f2 . n = H₁(f2 | n)

proof

let n be Nat; :: thesis: f2 . n = H₁(f2 | n)
( n = 0 or n + 1 > 0 + 1 ) by XREAL_1:6;
then ( n = 0 or n >= 1 ) by NAT_1:13;
then ( n = 0 or n = 1 or n > 1 ) by XXREAL_0:1;
then A87: ( n = 0 or n = 1 or n + 1 > 1 + 1 ) by XREAL_1:6;

per cases ( n = 0 or n = 1 or n >= 2 ) by A87, NAT_1:13;

suppose A88: n = 0 ; :: thesis: f2 . n = H₁(f2 | n)

hence f2 . n = F . {} by A65, A66, A62
.= H₁(f2 | n) by A88 ;
:: thesis: verum

end;

suppose A89: n = 1 ; :: thesis: f2 . n = H₁(f2 | n)

1 c= NAT ;
then 1 c= dom f2 by FUNCT_2:def 1;
then A90: dom (f2 | 1) = 1 by RELAT_1:62;
f2 | 1 in (bool (the_universe_of (X \/ NAT))) ^omega by AFINSQ_1:42;
hence f2 . n = H₁(f2 | n) by A90, A10, A89, A63; :: thesis: verum

end;

suppose A91: n >= 2 ; :: thesis: f2 . n = H₁(f2 | n)

n c= NAT ;
then n c= dom f2 by FUNCT_2:def 1;
then A92: dom (f2 | n) = n by RELAT_1:62;
f2 | n in (bool (the_universe_of (X \/ NAT))) ^omega by AFINSQ_1:42;
then consider fs1 being FinSequence such that
A93: ( len fs1 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs1 . p = [:((f2 | n) . p),((f2 | n) . (n - p)):] ) & F . (f2 | n) = Union (disjoin fs1) ) by A91, A92, A10;
consider fs2 being FinSequence such that
A94: ( len fs2 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs2 . p = [:(f2 . p),(f2 . (n - p)):] ) & f2 . n = Union (disjoin fs2) ) by A91, A64;
for p being Nat st 1 <= p & p <= len fs1 holds
fs1 . p = fs2 . p

proof

let p be Nat; :: thesis: ( 1 <= p & p <= len fs1 implies fs1 . p = fs2 . p )
assume A95: ( 1 <= p & p <= len fs1 ) ; :: thesis: fs1 . p = fs2 . p
then A96: fs1 . p = [:((f2 | n) . p),((f2 | n) . (n - p)):] by A93;
A97: fs2 . p = [:(f2 . p),(f2 . (n - p)):] by A95, A93, A94;
set n9 = n -' 1;
n - 1 >= 2 - 1 by A91, XREAL_1:9;
then A98: n -' 1 = n - 1 by XREAL_0:def 2;
then A99: p in Seg (n -' 1) by A95, A93, FINSEQ_1:1;
A100: Seg (n -' 1) c= Segm ((n -' 1) + 1) by AFINSQ_1:3;
( - p <= - 1 & - p >= - (n - 1) ) by A95, A93, XREAL_1:24;
then A101: ( (- p) + n <= (- 1) + n & (- p) + n >= (- (n - 1)) + n ) by XREAL_1:6;
then A102: ( n - p <= n -' 1 & n - p >= 1 ) by XREAL_0:def 2;
A103: n - p = n -' p by A101, XREAL_0:def 2;
then A104: n -' p in Seg (n -' 1) by A102, FINSEQ_1:1;
Seg (n -' 1) c= Segm ((n -' 1) + 1) by AFINSQ_1:3;
then (f2 | n) . (n - p) = f2 . (n - p) by A104, A103, A98, FUNCT_1:49;
hence fs1 . p = fs2 . p by A100, A96, A97, A98, A99, FUNCT_1:49; :: thesis: verum

end;

hence f2 . n = H₁(f2 | n) by A94, A93, FINSEQ_1:14; :: thesis: verum

end;

end;

end;

f1 = f2 from ALGSTR_4:sch 3(A67, A86);
hence f1 = f2 ; :: thesis: verum