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 A61: 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 A62: 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 A63: 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 A64: 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 A65: 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 A66: 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:47;
then A67: ( S1[ {} ,F . {}] & {} is XFinSequence of ) by A11, AFINSQ_1:46;
A68: dom {} = {} ;
A69: for n being natural number holds f1 . n = H1(f1 | n)
proof
let n be natural number ; :: thesis: f1 . n = H1(f1 | n)
( n = 0 or n + 1 > 0 + 1 ) by XREAL_1:8;
then ( n = 0 or n >= 1 ) by NAT_1:13;
then ( n = 0 or n = 1 or n > 1 ) by XXREAL_0:1;
then A70: ( n = 0 or n = 1 or n + 1 > 1 + 1 ) by XREAL_1:8;
per cases ( n = 0 or n = 1 or n >= 2 ) by A70, NAT_1:13;
suppose A71: n = 0 ; :: thesis: f1 . n = H1(f1 | n)
hence f1 . n = F . {} by A67, A68, A61
.= H1(f1 | n) by A71 ;
:: thesis: verum
end;
suppose A75: n >= 2 ; :: thesis: f1 . n = H1(f1 | n)
n c= NAT ;
then n c= dom f1 by FUNCT_2:def 1;
then A76: dom (f1 | n) = n by RELAT_1:91;
f1 | n in (bool (the_universe_of (X \/ NAT))) ^omega by AFINSQ_1:46;
then consider fs1 being FinSequence such that
A77: ( 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 A75, A76, A11;
consider fs2 being FinSequence such that
A78: ( 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 A75, A63;
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 A80: ( 1 <= p & p <= len fs1 ) ; :: thesis: fs1 . p = fs2 . p
then A81: fs1 . p = [:((f1 | n) . p),((f1 | n) . (n - p)):] by A77;
A82: fs2 . p = [:(f1 . p),(f1 . (n - p)):] by A80, A77, A78;
set n9 = n -' 1;
n - 1 >= 2 - 1 by A75, XREAL_1:11;
then A83: n -' 1 = n - 1 by XREAL_0:def 2;
then A84: p in Seg (n -' 1) by A80, A77, FINSEQ_1:3;
A85: Seg (n -' 1) c= (n -' 1) + 1 by AFINSQ_1:5;
( - p <= - 1 & - p >= - (n - 1) ) by A80, A77, XREAL_1:26;
then A86: ( (- p) + n <= (- 1) + n & (- p) + n >= (- (n - 1)) + n ) by XREAL_1:8;
then A87: ( n - p <= n -' 1 & n - p >= 1 ) by XREAL_0:def 2;
A88: n - p = n -' p by A86, XREAL_0:def 2;
then A89: n -' p in Seg (n -' 1) by A87, FINSEQ_1:3;
Seg (n -' 1) c= (n -' 1) + 1 by AFINSQ_1:5;
then (f1 | n) . (n - p) = f1 . (n - p) by A88, A83, A89, FUNCT_1:72;
hence fs1 . p = fs2 . p by A85, A81, A82, A83, A84, FUNCT_1:72; :: thesis: verum
end;
hence f1 . n = H1(f1 | n) by A77, A78, FINSEQ_1:18; :: thesis: verum
end;
end;
end;
A91: for n being natural number holds f2 . n = H1(f2 | n)
proof
let n be natural number ; :: thesis: f2 . n = H1(f2 | n)
( n = 0 or n + 1 > 0 + 1 ) by XREAL_1:8;
then ( n = 0 or n >= 1 ) by NAT_1:13;
then ( n = 0 or n = 1 or n > 1 ) by XXREAL_0:1;
then A92: ( n = 0 or n = 1 or n + 1 > 1 + 1 ) by XREAL_1:8;
per cases ( n = 0 or n = 1 or n >= 2 ) by A92, NAT_1:13;
suppose A93: n = 0 ; :: thesis: f2 . n = H1(f2 | n)
hence f2 . n = F . {} by A67, A68, A64
.= H1(f2 | n) by A93 ;
:: thesis: verum
end;
suppose A97: n >= 2 ; :: thesis: f2 . n = H1(f2 | n)
n c= NAT ;
then n c= dom f2 by FUNCT_2:def 1;
then A98: dom (f2 | n) = n by RELAT_1:91;
f2 | n in (bool (the_universe_of (X \/ NAT))) ^omega by AFINSQ_1:46;
then consider fs1 being FinSequence such that
A99: ( 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 A97, A98, A11;
consider fs2 being FinSequence such that
A100: ( 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 A97, A66;
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 A102: ( 1 <= p & p <= len fs1 ) ; :: thesis: fs1 . p = fs2 . p
then A103: fs1 . p = [:((f2 | n) . p),((f2 | n) . (n - p)):] by A99;
A104: fs2 . p = [:(f2 . p),(f2 . (n - p)):] by A102, A99, A100;
set n9 = n -' 1;
n - 1 >= 2 - 1 by A97, XREAL_1:11;
then A105: n -' 1 = n - 1 by XREAL_0:def 2;
then A106: p in Seg (n -' 1) by A102, A99, FINSEQ_1:3;
A107: Seg (n -' 1) c= (n -' 1) + 1 by AFINSQ_1:5;
( - p <= - 1 & - p >= - (n - 1) ) by A102, A99, XREAL_1:26;
then A108: ( (- p) + n <= (- 1) + n & (- p) + n >= (- (n - 1)) + n ) by XREAL_1:8;
then A109: ( n - p <= n -' 1 & n - p >= 1 ) by XREAL_0:def 2;
A110: n - p = n -' p by A108, XREAL_0:def 2;
then A111: n -' p in Seg (n -' 1) by A109, FINSEQ_1:3;
Seg (n -' 1) c= (n -' 1) + 1 by AFINSQ_1:5;
then (f2 | n) . (n - p) = f2 . (n - p) by A111, A110, A105, FUNCT_1:72;
hence fs1 . p = fs2 . p by A107, A103, A104, A105, A106, FUNCT_1:72; :: thesis: verum
end;
hence f2 . n = H1(f2 | n) by FINSEQ_1:18, A100, A99; :: thesis: verum
end;
end;
end;
f1 = f2 from ALGSTR_4:sch 3(A69, A91);
 hence f1 = f2 ; :: thesis: verum