deffunc H1( Nat, Subset of F1()) -> Subset of F1() = F4($2);
consider f being sequence of (bool F1()) such that
A4: f . 0 = F3() and
A5: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch 12();
 defpred S1[ Nat] means f . $1 c= F2();
A6: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; :: thesis: S1[n + 1]
f . (n + 1) = F4((f . n)) by A5;
hence S1[n + 1] by A3, A7; :: thesis: verum
end;
A8: S1[ 0 ] by A2, A4;
A9: for n being Nat holds S1[n] from NAT_1:sch 2(A8, A6);
 A10: for i being Nat holds f . i c= f . (i + 1)
proof
let i be Nat; :: thesis: f . i c= f . (i + 1)
( f . (i + 1) = F4((f . i)) & f . i c= F2() ) by A5, A9;
hence f . i c= f . (i + 1) by A3; :: thesis: verum
end;
A11: dom f = NAT by FUNCT_2:def 1;
A12: rng f is c=-linear
proof
let B, C be set ; :: according to ORDINAL1:def 8 :: thesis: ( not B in rng f or not C in rng f or B,C are_c=-comparable )
assume B in rng f ; :: thesis: ( not C in rng f or B,C are_c=-comparable )
then consider i being object such that
A13: i in NAT and
A14: B = f . i by A11, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A13;
assume C in rng f ; :: thesis: B,C are_c=-comparable
then consider j being object such that
A15: j in NAT and
A16: C = f . j by A11, FUNCT_1:def 3;
reconsider j = j as Element of NAT by A15;
( i <= j or j <= i ) ;
hence ( B c= C or C c= B ) by A10, A14, A16, MEASURE2:18; :: according to XBOOLE_0:def 9 :: thesis: verum
end;
A17: rng f c= bool F2()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in bool F2() )
reconsider xx = x as set by TARSKI:1;
assume x in rng f ; :: thesis: x in bool F2()
then x in f .: NAT by RELSET_1:22;
then ex k being Element of NAT st
( k in NAT & f . k = x ) by FUNCT_2:65;
then xx c= F2() by A9;
hence x in bool F2() ; :: thesis: verum
end;
rng f <> {} by A4, A11, FUNCT_1:def 3;
then consider m being set such that
A18: m in rng f and
A19: for C being set st C in rng f holds
C c= m by A1, A17, A12, FINSET_1:12;
deffunc H2( Nat) -> Element of bool F1() = f . |.($1 - 1).|;
defpred S2[ set ] means ( $1 in NAT & f . $1 = m );
m in f .: NAT by A18, RELSET_1:22;
then ex k being Element of NAT st S2[k] by FUNCT_2:65;
then A20: ex k being Nat st S2[k] ;
consider k being Nat such that
A21: S2[k] and
A22: for n being Nat st S2[n] holds
k <= n from NAT_1:sch 5(A20);
 consider z being FinSequence of bool F1() such that
A23: len z = k + 1 and
A24: for j being Nat st j in dom z holds
z . j = H2(j) from FINSEQ_2:sch 1();
 A25: 0 + 1 <= len z by A23, NAT_1:13;
then A26: 1 in Seg (k + 1) by A23, FINSEQ_1:1;
take z ; :: thesis: ( len z > 0 & z /. 1 = F3() & ( for i being Nat st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ) & F4((z /. (len z))) = z /. (len z) & ( for i, j being Nat st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
thus 0 < len z by A23; :: thesis: ( z /. 1 = F3() & ( for i being Nat st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ) & F4((z /. (len z))) = z /. (len z) & ( for i, j being Nat st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
A27: dom z = Seg (k + 1) by A23, FINSEQ_1:def 3;
thus z /. 1 = z . 1 by A25, FINSEQ_4:15
.= f . |.(1 - 1).| by A24, A27, A26
.= F3() by A4, ABSVALUE:2 ; :: thesis: ( ( for i being Nat st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ) & F4((z /. (len z))) = z /. (len z) & ( for i, j being Nat st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
thus A28: for i being Nat st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) :: thesis: ( F4((z /. (len z))) = z /. (len z) & ( for i, j being Nat st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
proof
let i be Nat; :: thesis: ( i > 0 & i < len z implies z /. (i + 1) = F4((z /. i)) )
assume that
A29: i > 0 and
A30: i < len z ; :: thesis: z /. (i + 1) = F4((z /. i))
A31: ( 0 + 1 < i + 1 & i + 1 <= k + 1 ) by A23, A29, A30, NAT_1:13, XREAL_1:6;
then A32: i + 1 in Seg (k + 1) by FINSEQ_1:1;
A33: 0 + 1 <= i by A29, NAT_1:13;
then i in Seg (k + 1) by A23, A30, FINSEQ_1:1;
then A34: ( z . i = f . |.(i - 1).| & i in dom z ) by A24, A27;
1 - 1 <= i - 1 by A33, XREAL_1:9;
then A35: 0 <= (i - 1) * 1 ;
thus z /. (i + 1) = z . (i + 1) by A23, A31, FINSEQ_4:15
.= f . |.((i + 1) - 1).| by A24, A27, A32
.= f . |.((i - 1) + 1).|
.= f . (|.(i - 1).| + |.1.|) by A35, ABSVALUE:11
.= f . (|.(i - 1).| + 1) by ABSVALUE:def 1
.= F4((f . |.(i - 1).|)) by A5
.= F4((z /. i)) by A34, PARTFUN1:def 6 ; :: thesis: verum
end;
thus F4((z /. (len z))) = z /. (len z) :: thesis: for i, j being Nat st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j )
proof
k + 1 in NAT ;
then k + 1 in dom f by FUNCT_2:def 1;
then f . (k + 1) in rng f by FUNCT_1:def 3;
then A36: f . (k + 1) c= f . k by A19, A21;
reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
A37: f . k c= f . (k + 1) by A10;
( len z = 0 or len z in Seg (len z) ) by FINSEQ_1:3;
then A38: len z in dom z by A23, FINSEQ_1:def 3;
A39: z . (len z) = f . |.((k + 1) - 1).| by A23, A24, A27, FINSEQ_1:3
.= f . k by ABSVALUE:def 1 ;
hence F4((z /. (len z))) = F4((f . k9)) by A38, PARTFUN1:def 6
.= f . (k + 1) by A5
.= z . (len z) by A37, A36, A39
.= z /. (len z) by A38, PARTFUN1:def 6 ;
:: thesis: verum
end;
let i, j be Nat; :: thesis: ( i > 0 & i < j & j <= len z implies ( z /. i c= F2() & z /. i c< z /. j ) )
assume that
A40: 0 < i and
A41: i < j and
A42: j <= len z ; :: thesis: ( z /. i c= F2() & z /. i c< z /. j )
A43: 0 + 1 <= i by A40, NAT_1:13;
then reconsider l = i - 1 as Element of NAT by INT_1:5;
A44: i <= len z by A41, A42, XXREAL_0:2;
then A45: i in Seg (k + 1) by A23, A43, FINSEQ_1:1;
A46: z /. i = z . i by A43, A44, FINSEQ_4:15
.= f . |.(i - 1).| by A24, A27, A45
.= f . l by ABSVALUE:def 1 ;
hence z /. i c= F2() by A9; :: thesis: z /. i c< z /. j
A47: for i being Nat st 1 <= i & i < len z holds
z /. i c= z /. (i + 1)
proof
let i be Nat; :: thesis: ( 1 <= i & i < len z implies z /. i c= z /. (i + 1) )
assume that
A48: 1 <= i and
A49: i < len z ; :: thesis: z /. i c= z /. (i + 1)
A50: i in Seg (k + 1) by A23, A48, A49, FINSEQ_1:1;
A51: 1 - 1 <= i - 1 by A48, XREAL_1:9;
then A52: i - 1 is Element of NAT by INT_1:3;
A53: ( 1 <= i + 1 & i + 1 <= len z ) by A48, A49, NAT_1:13;
then A54: i + 1 in Seg (k + 1) by A23, FINSEQ_1:1;
A55: z /. (i + 1) = z . (i + 1) by A53, FINSEQ_4:15
.= f . |.((i + 1) - 1).| by A24, A27, A54
.= f . ((i - 1) + 1) by ABSVALUE:def 1 ;
z /. i = z . i by A48, A49, FINSEQ_4:15
.= f . |.(i - 1).| by A24, A27, A50
.= f . (i - 1) by A51, ABSVALUE:def 1 ;
hence z /. i c= z /. (i + 1) by A10, A55, A52; :: thesis: verum
end;
hence z /. i c= z /. j by A41, A42, A43, Th1; :: according to XBOOLE_0:def 8 :: thesis: not z /. i = z /. j
defpred S3[ Nat] means ( i + $1 <= len z implies z /. i = z /. (i + $1) );
A56: ( i <= i + 1 & i + 1 <= j ) by A41, NAT_1:13;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A57: k + 1 in dom z by A23, FINSEQ_1:def 3;
A58: i < len z by A41, A42, XXREAL_0:2;
assume z /. i = z /. j ; :: thesis: contradiction
then A59: z /. i = z /. (i + 1) by A42, A43, A47, A56, Th2
.= F4((z /. i)) by A28, A40, A58 ;
A60: now :: thesis: for n being Nat st S3[n] holds
S3[n + 1]
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume A61: S3[n] ; :: thesis: S3[n + 1]
thus S3[n + 1] :: thesis: verum
proof
assume i + (n + 1) <= len z ; :: thesis: z /. i = z /. (i + (n + 1))
then (i + n) + 1 <= len z ;
then i + n < len z by NAT_1:13;
hence z /. i = z /. ((i + n) + 1) by A28, A40, A59, A61
.= z /. (i + (n + 1)) ;
:: thesis: verum
end;
end;
consider n0 being Nat such that
A62: i + n0 = len z by A41, A42, NAT_1:10, XXREAL_0:2;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 12;
A63: i + n0 = len z by A62;
A64: S3[ 0 ] ;
for n being Nat holds S3[n] from NAT_1:sch 2(A64, A60);
 then f . l = z /. (k + 1) by A23, A46, A63
.= z . (k + 1) by A57, PARTFUN1:def 6
.= f . |.((k + 1) - 1).| by A24, A27, FINSEQ_1:4
.= m by A21, ABSVALUE:def 1 ;
then k <= l by A22;
then len z <= l + 1 by A23, XREAL_1:6;
hence contradiction by A41, A42, XXREAL_0:2; :: thesis: verum