let f1, f2 be sequence of (bool (the_universe_of (X \/ NAT))); ( 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 = {}
; ( 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
; ( 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) )
; ( 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 = {}
; ( 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
; ( 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) )
; f1 = f2
{} in (bool (the_universe_of (X \/ NAT))) ^omega
by AFINSQ_1:43;
then A65:
( S1[ {} ,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 H1( 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 = H1(f1 | n)
proof
let n be
Nat;
f1 . n = H1(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 A72:
n >= 2
;
f1 . n = H1(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;
( 1 <= p & p <= len fs1 implies fs1 . p = fs2 . p )
assume A76:
( 1
<= p &
p <= len fs1 )
;
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;
verum
end; hence
f1 . n = H1(
f1 | n)
by A74, A75, FINSEQ_1:14;
verum end; end;
end;
A86:
for n being Nat holds f2 . n = H1(f2 | n)
proof
let n be
Nat;
f2 . n = H1(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 A91:
n >= 2
;
f2 . n = H1(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;
( 1 <= p & p <= len fs1 implies fs1 . p = fs2 . p )
assume A95:
( 1
<= p &
p <= len fs1 )
;
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;
verum
end; hence
f2 . n = H1(
f2 | n)
by A94, A93, FINSEQ_1:14;
verum end; end;
end;
f1 = f2
from ALGSTR_4:sch 3(A67, A86);
hence
f1 = f2
; verum