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