let f1, f2 be Function of NAT,(bool (the_universe_of (X \/ NAT))); :: thesis: ( f1 . 0 = {} & f1 . 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 = [:(f1 . p),(f1 . (n - p)):] ) & f1 . n = Union (disjoin fs) ) ) & f2 . 0 = {} & f2 . 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 = [:(f2 . p),(f2 . (n - p)):] ) & f2 . n = Union (disjoin fs) ) ) implies f1 = f2 )
assume A60: f1 . 0 = {} ; :: thesis: ( not f1 . 1 = X or ex n being natural number st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being natural number 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 natural number st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being natural number 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: f1 . 1 = X ; :: thesis: ( ex n being natural number st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being natural number 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 natural number st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being natural number 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: 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 = [:(f1 . p),(f1 . (n - p)):] ) & f1 . n = Union (disjoin fs) ) ; :: thesis: ( not f2 . 0 = {} or not f2 . 1 = X or ex n being natural number st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being natural number 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 . 0 = {} ; :: thesis: ( not f2 . 1 = X or ex n being natural number st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being natural number 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: f2 . 1 = X ; :: thesis: ( ex n being natural number st
( n >= 2 & ( for fs being FinSequence holds
( not len fs = n - 1 or ex p being natural number 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 A65: 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 = [:(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 A66: ( S₁[ {} ,F . {}] & {} is XFinSequence of ) by A11, AFINSQ_1:42;
A67: dom {} = {} ;
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;
A68: for n being natural number holds f1 . n = H₁(f1 | n)

proof

let n be natural number ; :: 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 A69: ( 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 A69, NAT_1:13;

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

hence f1 . n = F . {} by A66, A67, A60
.= H₁(f1 | n) by A70 ;
:: thesis: verum

end;

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

1 c= NAT ;
then 1 c= dom f1 by FUNCT_2:def 1;
then A72: 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 A71, A72, A11, A61; :: thesis: verum

end;

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

n c= NAT ;
then n c= dom f1 by FUNCT_2:def 1;
then A74: 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
A75: ( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs1 . p = [:((f1 | n) . p),((f1 | n) . (n - p)):] ) & F . (f1 | n) = Union (disjoin fs1) ) by A73, A74, A11;
consider fs2 being FinSequence such that
A76: ( len fs2 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs2 . p = [:(f1 . p),(f1 . (n - p)):] ) & f1 . n = Union (disjoin fs2) ) by A73, A62;
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 A77: ( 1 <= p & p <= len fs1 ) ; :: thesis: fs1 . p = fs2 . p
then A78: fs1 . p = [:((f1 | n) . p),((f1 | n) . (n - p)):] by A75;
A79: fs2 . p = [:(f1 . p),(f1 . (n - p)):] by A77, A75, A76;
set n9 = n -' 1;
n - 1 >= 2 - 1 by A73, XREAL_1:9;
then A80: n -' 1 = n - 1 by XREAL_0:def 2;
then A81: p in Seg (n -' 1) by A77, A75, FINSEQ_1:1;
A82: Seg (n -' 1) c= (n -' 1) + 1 by AFINSQ_1:3;
( - p <= - 1 & - p >= - (n - 1) ) by A77, A75, XREAL_1:24;
then A83: ( (- p) + n <= (- 1) + n & (- p) + n >= (- (n - 1)) + n ) by XREAL_1:6;
then A84: ( n - p <= n -' 1 & n - p >= 1 ) by XREAL_0:def 2;
A85: n - p = n -' p by A83, XREAL_0:def 2;
then A86: n -' p in Seg (n -' 1) by A84, FINSEQ_1:1;
Seg (n -' 1) c= (n -' 1) + 1 by AFINSQ_1:3;
then (f1 | n) . (n - p) = f1 . (n - p) by A85, A80, A86, FUNCT_1:49;
hence fs1 . p = fs2 . p by A82, A78, A79, A80, A81, FUNCT_1:49; :: thesis: verum

end;

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

end;

end;

end;

A87: for n being natural number holds f2 . n = H₁(f2 | n)

proof

let n be natural number ; :: 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 A88: ( 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 A88, NAT_1:13;

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

hence f2 . n = F . {} by A66, A67, A63
.= H₁(f2 | n) by A89 ;
:: thesis: verum

end;

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

1 c= NAT ;
then 1 c= dom f2 by FUNCT_2:def 1;
then A91: 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 A91, A11, A90, A64; :: thesis: verum

end;

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

n c= NAT ;
then n c= dom f2 by FUNCT_2:def 1;
then A93: 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
A94: ( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs1 . p = [:((f2 | n) . p),((f2 | n) . (n - p)):] ) & F . (f2 | n) = Union (disjoin fs1) ) by A92, A93, A11;
consider fs2 being FinSequence such that
A95: ( len fs2 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs2 . p = [:(f2 . p),(f2 . (n - p)):] ) & f2 . n = Union (disjoin fs2) ) by A92, A65;
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 A96: ( 1 <= p & p <= len fs1 ) ; :: thesis: fs1 . p = fs2 . p
then A97: fs1 . p = [:((f2 | n) . p),((f2 | n) . (n - p)):] by A94;
A98: fs2 . p = [:(f2 . p),(f2 . (n - p)):] by A96, A94, A95;
set n9 = n -' 1;
n - 1 >= 2 - 1 by A92, XREAL_1:9;
then A99: n -' 1 = n - 1 by XREAL_0:def 2;
then A100: p in Seg (n -' 1) by A96, A94, FINSEQ_1:1;
A101: Seg (n -' 1) c= (n -' 1) + 1 by AFINSQ_1:3;
( - p <= - 1 & - p >= - (n - 1) ) by A96, A94, XREAL_1:24;
then A102: ( (- p) + n <= (- 1) + n & (- p) + n >= (- (n - 1)) + n ) by XREAL_1:6;
then A103: ( n - p <= n -' 1 & n - p >= 1 ) by XREAL_0:def 2;
A104: n - p = n -' p by A102, XREAL_0:def 2;
then A105: n -' p in Seg (n -' 1) by A103, FINSEQ_1:1;
Seg (n -' 1) c= (n -' 1) + 1 by AFINSQ_1:3;
then (f2 | n) . (n - p) = f2 . (n - p) by A105, A104, A99, FUNCT_1:49;
hence fs1 . p = fs2 . p by A101, A97, A98, A99, A100, FUNCT_1:49; :: thesis: verum

end;

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

end;

end;

end;

f1 = f2 from ALGSTR_4:sch 3(A68, A87);
hence f1 = f2 ; :: thesis: verum