deffunc H_{1}( Nat, Subset of F_{1}()) -> Subset of F_{1}() = F_{4}($2);

consider f being sequence of (bool F_{1}()) such that

A4: f . 0 = F_{3}()
and

A5: for n being Nat holds f . (n + 1) = H_{1}(n,f . n)
from NAT_1:sch 12();

defpred S_{1}[ Nat] means f . $1 c= F_{2}();

_{1}[ 0 ]
by A2, A4;

A9: for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A8, A6);

A10: for i being Nat holds f . i c= f . (i + 1)

A12: rng f is c=-linear_{2}()

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 H_{2}( Nat) -> Element of bool F_{1}() = f . |.($1 - 1).|;

defpred S_{2}[ 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 S_{2}[k]
by FUNCT_2:65;

then A20: ex k being Nat st S_{2}[k]
;

consider k being Nat such that

A21: S_{2}[k]
and

A22: for n being Nat st S_{2}[n] holds

k <= n from NAT_1:sch 5(A20);

consider z being FinSequence of bool F_{1}() such that

A23: len z = k + 1 and

A24: for j being Nat st j in dom z holds

z . j = H_{2}(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 = F_{3}() & ( for i being Nat st i > 0 & i < len z holds

z /. (i + 1) = F_{4}((z /. i)) ) & F_{4}((z /. (len z))) = z /. (len z) & ( for i, j being Nat st i > 0 & i < j & j <= len z holds

( z /. i c= F_{2}() & z /. i c< z /. j ) ) )

thus 0 < len z by A23; :: thesis: ( z /. 1 = F_{3}() & ( for i being Nat st i > 0 & i < len z holds

z /. (i + 1) = F_{4}((z /. i)) ) & F_{4}((z /. (len z))) = z /. (len z) & ( for i, j being Nat st i > 0 & i < j & j <= len z holds

( z /. i c= F_{2}() & 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

.= F_{3}()
by A4, ABSVALUE:2
; :: thesis: ( ( for i being Nat st i > 0 & i < len z holds

z /. (i + 1) = F_{4}((z /. i)) ) & F_{4}((z /. (len z))) = z /. (len z) & ( for i, j being Nat st i > 0 & i < j & j <= len z holds

( z /. i c= F_{2}() & z /. i c< z /. j ) ) )

thus A28: for i being Nat st i > 0 & i < len z holds

z /. (i + 1) = F_{4}((z /. i))
:: thesis: ( F_{4}((z /. (len z))) = z /. (len z) & ( for i, j being Nat st i > 0 & i < j & j <= len z holds

( z /. i c= F_{2}() & z /. i c< z /. j ) ) )_{4}((z /. (len z))) = z /. (len z)
:: thesis: for i, j being Nat st i > 0 & i < j & j <= len z holds

( z /. i c= F_{2}() & z /. i c< z /. j )_{2}() & z /. i c< z /. j ) )

assume that

A40: 0 < i and

A41: i < j and

A42: j <= len z ; :: thesis: ( z /. i c= F_{2}() & 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= F_{2}()
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)

defpred S_{3}[ 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

.= F_{4}((z /. i))
by A28, A40, A58
;

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: S_{3}[ 0 ]
;

for n being Nat holds S_{3}[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

consider f being sequence of (bool F

A4: f . 0 = F

A5: for n being Nat holds f . (n + 1) = H

defpred S

A6: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

A8:
SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A7: S_{1}[n]
; :: thesis: S_{1}[n + 1]

f . (n + 1) = F_{4}((f . n))
by A5;

hence S_{1}[n + 1]
by A3, A7; :: thesis: verum

end;assume A7: S

f . (n + 1) = F

hence S

A9: for n being Nat holds S

A10: for i being Nat holds f . i c= f . (i + 1)

proof

A11:
dom f = NAT
by FUNCT_2:def 1;
let i be Nat; :: thesis: f . i c= f . (i + 1)

( f . (i + 1) = F_{4}((f . i)) & f . i c= F_{2}() )
by A5, A9;

hence f . i c= f . (i + 1) by A3; :: thesis: verum

end;( f . (i + 1) = F

hence f . i c= f . (i + 1) by A3; :: thesis: verum

A12: rng f is c=-linear

proof

A17:
rng f c= bool F
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;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

proof

rng f <> {}
by A4, A11, FUNCT_1:def 3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in bool F_{2}() )

reconsider xx = x as set by TARSKI:1;

assume x in rng f ; :: thesis: x in bool F_{2}()

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= F_{2}()
by A9;

hence x in bool F_{2}()
; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume x in rng f ; :: thesis: x in bool F

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= F

hence x in bool F

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 H

defpred S

m in f .: NAT by A18, RELSET_1:22;

then ex k being Element of NAT st S

then A20: ex k being Nat st S

consider k being Nat such that

A21: S

A22: for n being Nat st S

k <= n from NAT_1:sch 5(A20);

consider z being FinSequence of bool F

A23: len z = k + 1 and

A24: for j being Nat st j in dom z holds

z . j = H

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 = F

z /. (i + 1) = F

( z /. i c= F

thus 0 < len z by A23; :: thesis: ( z /. 1 = F

z /. (i + 1) = F

( z /. i c= F

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

.= F

z /. (i + 1) = F

( z /. i c= F

thus A28: for i being Nat st i > 0 & i < len z holds

z /. (i + 1) = F

( z /. i c= F

proof

thus
F
let i be Nat; :: thesis: ( i > 0 & i < len z implies z /. (i + 1) = F_{4}((z /. i)) )

assume that

A29: i > 0 and

A30: i < len z ; :: thesis: z /. (i + 1) = F_{4}((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

.= F_{4}((f . |.(i - 1).|))
by A5

.= F_{4}((z /. i))
by A34, PARTFUN1:def 6
; :: thesis: verum

end;assume that

A29: i > 0 and

A30: i < len z ; :: thesis: z /. (i + 1) = F

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

.= F

.= F

( z /. i c= F

proof

let i, j be Nat; :: thesis: ( i > 0 & i < j & j <= len z implies ( z /. i c= F
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 F_{4}((z /. (len z))) =
F_{4}((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;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 F

.= f . (k + 1) by A5

.= z . (len z) by A37, A36, A39

.= z /. (len z) by A38, PARTFUN1:def 6 ;

:: thesis: verum

assume that

A40: 0 < i and

A41: i < j and

A42: j <= len z ; :: thesis: ( z /. i c= F

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= F

A47: for i being Nat st 1 <= i & i < len z holds

z /. i c= z /. (i + 1)

proof

hence
z /. i c= z /. j
by A41, A42, A43, Th1; :: according to XBOOLE_0:def 8 :: thesis: not z /. i = z /. j
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;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

defpred S

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

.= F

A60: now :: thesis: for n being Nat st S_{3}[n] holds

S_{3}[n + 1]

consider n0 being Nat such that S

let n be Nat; :: thesis: ( S_{3}[n] implies S_{3}[n + 1] )

assume A61: S_{3}[n]
; :: thesis: S_{3}[n + 1]

thus S_{3}[n + 1]
:: thesis: verum

end;assume A61: S

thus S

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: S

for n being Nat holds S

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