let n, i be Element of NAT ; :: thesis: ( i < n implies ( (n -BinarySequence (2 to_power i)) . (i + 1) = 1 & ( for j being Element of NAT st j in Seg n & j <> i + 1 holds
(n -BinarySequence (2 to_power i)) . j = 0 ) ) )
assume A1: i < n ; :: thesis: ( (n -BinarySequence (2 to_power i)) . (i + 1) = 1 & ( for j being Element of NAT st j in Seg n & j <> i + 1 holds
(n -BinarySequence (2 to_power i)) . j = 0 ) )
set B = n -BinarySequence (2 to_power i);
deffunc H₁( Nat) -> Element of $1 -tuples_on BOOLEAN = $1 -BinarySequence (2 to_power i);
defpred S₁[ Nat] means ( i < $1 implies H₁($1) . (i + 1) = TRUE );
A2: S₁[ 0 ] ;

A3: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]

now

assume Z: i < n + 1 ; :: thesis: H₁(n + 1) . (i + 1) = TRUE
then A5: i <= n by NAT_1:13;

per cases ( n = 0 or ( n > 0 & n = i ) or ( n > 0 & n > i ) ) by A5, XXREAL_0:1;

suppose A6: n = 0 ; :: thesis: H₁(n + 1) . (i + 1) = TRUE

then A7: i = 0 by Z, NAT_1:13;
0* n = n |-> 0 by EUCLID:def 4;
then dom (0* n) = Seg n by FUNCOP_1:19;
then A8: len (0* n) = n by FINSEQ_1:def 3;
dom <*TRUE *> = Seg 1 by FINSEQ_1:55;
then A9: 1 in dom <*TRUE *> by FINSEQ_1:3;
thus H₁(n + 1) . (i + 1) = ((0* n) ^ <*TRUE *>) . (i + 1) by A6, A7, BINARI_3:29
.= <*TRUE *> . 1 by A6, A7, A8, A9, FINSEQ_1:def 7
.= TRUE by FINSEQ_1:57 ; :: thesis: verum

end;

suppose A10: ( n > 0 & n = i ) ; :: thesis: H₁(n + 1) . (i + 1) = TRUE

0* n = n |-> 0 by EUCLID:def 4;
then dom (0* n) = Seg n by FUNCOP_1:19;
then A11: len (0* n) = n by FINSEQ_1:def 3;
dom <*TRUE *> = Seg 1 by FINSEQ_1:55;
then A12: 1 in dom <*TRUE *> by FINSEQ_1:3;
thus H₁(n + 1) . (i + 1) = ((0* n) ^ <*TRUE *>) . (i + 1) by A10, BINARI_3:29
.= <*TRUE *> . 1 by A10, A11, A12, FINSEQ_1:def 7
.= TRUE by FINSEQ_1:57 ; :: thesis: verum

end;

suppose A13: ( n > 0 & n > i ) ; :: thesis: H₁(n + 1) . (i + 1) = TRUE

then reconsider n' = n as non empty Element of NAT ;
A14: 2 to_power i < 2 to_power n by A13, POWER:44;
A15: 0 + 1 <= i + 1 by XREAL_1:8;
i + 1 <= n by A13, NAT_1:13;
then i + 1 in Seg n by A15, FINSEQ_1:3;
then A16: i + 1 in dom H₁(n) by Lm1;
thus H₁(n + 1) . (i + 1) = (H₁(n') ^ <*FALSE *>) . (i + 1) by A14, BINARI_3:28
.= TRUE by A4, A13, A16, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A17: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
defpred S₂[ Element of NAT ] means ( i < $1 implies for j being Element of NAT st i + 1 <= j & j <= $1 holds
H₁($1) . (j + 1) = FALSE );
A18: S₂[ 0 ] ;

A19: now

let n be Element of NAT ; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A20: S₂[n] ; :: thesis: S₂[n + 1]

now

assume A21: i < n + 1 ; :: thesis: for j being Element of NAT st i + 1 <= j & j <= n + 1 holds
H₁(n + 1) . (b₂ + 1) = FALSE
let j be Element of NAT ; :: thesis: ( i + 1 <= j & j <= n + 1 implies H₁(n + 1) . (b₁ + 1) = FALSE )
assume A22: ( i + 1 <= j & j <= n + 1 ) ; :: thesis: H₁(n + 1) . (b₁ + 1) = FALSE
A23: i <= n by A21, NAT_1:13;
A24: 0 + 1 <= i + 1 by XREAL_1:8;

per cases ( n = 0 or ( n > 0 & n = i ) or ( n > 0 & n > i ) ) by A23, XXREAL_0:1;

suppose A25: n = 0 ; :: thesis: H₁(n + 1) . (b₁ + 1) = FALSE

A26: dom H₁(n + 1) = Seg (n + 1) by Lm1;
1 <= j by A22, A24, XXREAL_0:2;
then j = 1 by A22, A25, XXREAL_0:1;
then not j + 1 in dom H₁(n + 1) by A25, A26, FINSEQ_1:3;
hence H₁(n + 1) . (j + 1) = FALSE by FUNCT_1:def 4; :: thesis: verum

end;

suppose A27: ( n > 0 & n = i ) ; :: thesis: H₁(n + 1) . (b₁ + 1) = FALSE

A28: dom H₁(n + 1) = Seg (n + 1) by Lm1;
j + 1 > n + 1 by A22, A27, NAT_1:13;
then not j + 1 in dom H₁(n + 1) by A28, FINSEQ_1:3;
hence H₁(n + 1) . (j + 1) = FALSE by FUNCT_1:def 4; :: thesis: verum

end;

suppose A29: ( n > 0 & n > i ) ; :: thesis: H₁(n + 1) . (b₁ + 1) = FALSE

then reconsider n' = n as non empty Element of NAT ;
A30: 2 to_power i < 2 to_power n by A29, POWER:44;
thus H₁(n + 1) . (j + 1) = FALSE :: thesis: verum

proof

( j < n + 1 or j = n + 1 ) by A22, XXREAL_0:1;
then A31: ( j <= n or j = n + 1 ) by NAT_1:13;

per cases ( j = n + 1 or j = n or j < n ) by A31, XXREAL_0:1;

suppose A32: j = n + 1 ; :: thesis: H₁(n + 1) . (j + 1) = FALSE

A33: dom H₁(n + 1) = Seg (n + 1) by Lm1;
j + 1 > n + 1 by A32, NAT_1:13;
then not j + 1 in dom H₁(n + 1) by A33, FINSEQ_1:3;
hence H₁(n + 1) . (j + 1) = FALSE by FUNCT_1:def 4; :: thesis: verum

end;

suppose A34: j = n ; :: thesis: H₁(n + 1) . (j + 1) = FALSE

dom H₁(n) = Seg n by Lm1;
then A35: j = len H₁(n) by A34, FINSEQ_1:def 3;
dom <*FALSE *> = Seg 1 by FINSEQ_1:55;
then A36: 1 in dom <*FALSE *> by FINSEQ_1:3;
thus H₁(n + 1) . (j + 1) = (H₁(n') ^ <*FALSE *>) . (j + 1) by A30, BINARI_3:28
.= <*FALSE *> . 1 by A35, A36, FINSEQ_1:def 7
.= FALSE by FINSEQ_1:57 ; :: thesis: verum

end;

suppose A37: j < n ; :: thesis: H₁(n + 1) . (j + 1) = FALSE

A38: 1 <= j + 1 by NAT_1:12;
j + 1 <= n by A37, NAT_1:13;
then j + 1 in Seg n by A38, FINSEQ_1:3;
then A39: j + 1 in dom H₁(n) by Lm1;
thus H₁(n + 1) . (j + 1) = (H₁(n') ^ <*FALSE *>) . (j + 1) by A30, BINARI_3:28
.= H₁(n) . (j + 1) by A39, FINSEQ_1:def 7
.= FALSE by A20, A22, A29, A37 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence S₂[n + 1] ; :: thesis: verum

end;

A40: for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A18, A19);
defpred S₃[ Element of NAT ] means ( i < $1 implies for j being Element of NAT st 1 <= j & j < i + 1 holds
H₁($1) . j = FALSE );
A41: S₃[ 0 ] ;

A42: now

let n be Element of NAT ; :: thesis: ( S₃[n] implies S₃[n + 1] )
assume A43: S₃[n] ; :: thesis: S₃[n + 1]

now

assume A44: i < n + 1 ; :: thesis: for j being Element of NAT st 1 <= j & j < i + 1 holds
H₁(n + 1) . b₂ = FALSE
let j be Element of NAT ; :: thesis: ( 1 <= j & j < i + 1 implies H₁(n + 1) . b₁ = FALSE )
assume A45: ( 1 <= j & j < i + 1 ) ; :: thesis: H₁(n + 1) . b₁ = FALSE
A46: i <= n by A44, NAT_1:13;

per cases ( n = 0 or ( n > 0 & i < n ) or ( n > 0 & i = n ) ) by A46, XXREAL_0:1;

suppose n = 0 ; :: thesis: H₁(n + 1) . b₁ = FALSE

then i = 0 by A44, NAT_1:13;
hence H₁(n + 1) . j = FALSE by A45; :: thesis: verum

end;

suppose A47: ( n > 0 & i < n ) ; :: thesis: H₁(n + 1) . b₁ = FALSE

then reconsider n' = n as non empty Element of NAT ;
A48: dom H₁(n) = Seg n by Lm1;
( j <= i & i <= n ) by A44, A45, NAT_1:13;
then j <= n by XXREAL_0:2;
then A49: j in dom H₁(n) by A45, A48, FINSEQ_1:3;
2 to_power i < 2 to_power n by A47, POWER:44;
hence H₁(n + 1) . j = (H₁(n') ^ <*FALSE *>) . j by BINARI_3:28
.= H₁(n) . j by A49, FINSEQ_1:def 7
.= FALSE by A43, A45, A47 ;
:: thesis: verum

end;

suppose A50: ( n > 0 & i = n ) ; :: thesis: H₁(n + 1) . b₁ = FALSE

then j <= n by A45, NAT_1:13;
then A51: j in Seg n by A45, FINSEQ_1:3;
A52: 0* n = n |-> 0 by EUCLID:def 4;
then A53: j in dom (0* n) by A51, FUNCOP_1:19;
thus H₁(n + 1) . j = ((0* n) ^ <*TRUE *>) . j by A50, BINARI_3:29
.= (0* n) . j by A53, FINSEQ_1:def 7
.= FALSE by A51, A52, FUNCOP_1:13 ; :: thesis: verum

end;

end;

end;

hence S₃[n + 1] ; :: thesis: verum

end;

A54: for n being Element of NAT holds S₃[n] from NAT_1:sch 1(A41, A42);
thus (n -BinarySequence (2 to_power i)) . (i + 1) = 1 by A1, A17; :: thesis: for j being Element of NAT st j in Seg n & j <> i + 1 holds
(n -BinarySequence (2 to_power i)) . j = 0
let j be Element of NAT ; :: thesis: ( j in Seg n & j <> i + 1 implies (n -BinarySequence (2 to_power i)) . j = 0 )
assume that
A55: j in Seg n and
A56: j <> i + 1 ; :: thesis: (n -BinarySequence (2 to_power i)) . j = 0
A57: ( 1 <= j & j <= n ) by A55, FINSEQ_1:3;

per cases ( j < i + 1 or ( j > i + 1 & j < n ) or ( j > i + 1 & j = n ) ) by A56, A57, XXREAL_0:1;

suppose j < i + 1 ; :: thesis: (n -BinarySequence (2 to_power i)) . j = 0

hence (n -BinarySequence (2 to_power i)) . j = 0 by A1, A54, A57; :: thesis: verum

end;

suppose A58: ( j > i + 1 & j < n ) ; :: thesis: (n -BinarySequence (2 to_power i)) . j = 0

then consider k being Nat such that
A59: j = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A60: i + 1 <= k by A58, A59, NAT_1:13;
k <= n by A58, A59, NAT_1:13;
hence (n -BinarySequence (2 to_power i)) . j = 0 by A1, A40, A59, A60; :: thesis: verum

end;

suppose A61: ( j > i + 1 & j = n ) ; :: thesis: (n -BinarySequence (2 to_power i)) . j = 0

then consider m being Nat such that
A62: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
i < m by A61, A62, XREAL_1:8;
then 2 to_power i < 2 to_power m by POWER:44;
hence (n -BinarySequence (2 to_power i)) . j = 0 by A61, A62, BINARI_3:27; :: thesis: verum

end;

end;