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 ) )
deffunc H₁( Nat) -> FinSequence of BOOLEAN = $1 -BinarySequence (2 to_power i);
set B = n -BinarySequence (2 to_power i);
defpred S₁[ Nat] means ( i < $1 implies H₁($1) . (i + 1) = TRUE );

A2: now

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

now

assume A4: 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

0* n = n |-> 0 by EUCLID:def 4;
then dom (0* n) = Seg n by FUNCOP_1:13;
then A7: len (0* n) = n by FINSEQ_1:def 3;
dom <*TRUE*> = Seg 1 by FINSEQ_1:38;
then A8: 1 in dom <*TRUE*> by FINSEQ_1:1;
A9: i = 0 by A4, A6, NAT_1:13;
hence H₁(n + 1) . (i + 1) = ((0* n) ^ <*TRUE*>) . (i + 1) by A6, BINARI_3:28
.= <*TRUE*> . 1 by A6, A9, A7, A8, FINSEQ_1:def 7
.= TRUE by FINSEQ_1:40 ;
:: 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:13;
then A11: len (0* n) = n by FINSEQ_1:def 3;
dom <*TRUE*> = Seg 1 by FINSEQ_1:38;
then A12: 1 in dom <*TRUE*> by FINSEQ_1:1;
thus H₁(n + 1) . (i + 1) = ((0* n) ^ <*TRUE*>) . (i + 1) by A10, BINARI_3:28
.= <*TRUE*> . 1 by A10, A11, A12, FINSEQ_1:def 7
.= TRUE by FINSEQ_1:40 ; :: thesis: verum

end;

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

then reconsider n9 = n as non empty Element of NAT ;
A14: 0 + 1 <= i + 1 by XREAL_1:6;
i + 1 <= n by A13, NAT_1:13;
then i + 1 in Seg n by A14, FINSEQ_1:1;
then A15: i + 1 in dom H₁(n) by Lm1;
2 to_power i < 2 to_power n by A13, POWER:39;
hence H₁(n + 1) . (i + 1) = (H₁(n9) ^ <*FALSE*>) . (i + 1) by BINARI_3:27
.= TRUE by A3, A13, A15, FINSEQ_1:def 7 ;
:: thesis: verum

end;

end;

end;

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

end;

A16: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A16, A2);
hence (n -BinarySequence (2 to_power i)) . (i + 1) = 1 by A1; :: thesis: for j being Element of NAT st j in Seg n & j <> i + 1 holds
(n -BinarySequence (2 to_power i)) . j = 0
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 );
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
A17: j in Seg n and
A18: j <> i + 1 ; :: thesis: (n -BinarySequence (2 to_power i)) . j = 0
A19: 1 <= j by A17, FINSEQ_1:1;

A20: now

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

now

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

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

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

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

end;

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

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

end;

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

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

proof

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

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

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

then A33: j + 1 > n + 1 by NAT_1:13;
dom H₁(n + 1) = Seg (n + 1) by Lm1;
then not j + 1 in dom H₁(n + 1) by A33, FINSEQ_1:1;
hence H₁(n + 1) . (j + 1) = FALSE by FUNCT_1:def 2; :: 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:38;
then A36: 1 in dom <*FALSE*> by FINSEQ_1:1;
thus H₁(n + 1) . (j + 1) = (H₁(n9) ^ <*FALSE*>) . (j + 1) by A31, BINARI_3:27
.= <*FALSE*> . 1 by A35, A36, FINSEQ_1:def 7
.= FALSE by FINSEQ_1:40 ; :: 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:1;
then A39: j + 1 in dom H₁(n) by Lm1;
thus H₁(n + 1) . (j + 1) = (H₁(n9) ^ <*FALSE*>) . (j + 1) by A31, BINARI_3:27
.= H₁(n) . (j + 1) by A39, FINSEQ_1:def 7
.= FALSE by A21, A24, A30, A37 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

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

end;

A40: S₂[ 0 ] ;
A41: for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A40, A20);
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 );

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
then A45: i <= n by NAT_1:13;
let j be Element of NAT ; :: thesis: ( 1 <= j & j < i + 1 implies H₁(n + 1) . b₁ = FALSE )
assume that
A46: 1 <= j and
A47: j < i + 1 ; :: thesis: H₁(n + 1) . b₁ = FALSE

per cases ( n = 0 or ( n > 0 & i < n ) or ( n > 0 & i = n ) ) by A45, 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 A46, A47; :: thesis: verum

end;

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

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

end;

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

then j <= n by A47, NAT_1:13;
then A53: j in Seg n by A46, FINSEQ_1:1;
A54: 0* n = n |-> 0 by EUCLID:def 4;
then A55: j in dom (0* n) by A53, FUNCOP_1:13;
thus H₁(n + 1) . j = ((0* n) ^ <*TRUE*>) . j by A52, BINARI_3:28
.= (0* n) . j by A55, FINSEQ_1:def 7
.= FALSE by A53, A54, FUNCOP_1:7 ; :: thesis: verum

end;

end;

end;

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

end;

A56: S₃[ 0 ] ;
A57: for n being Element of NAT holds S₃[n] from NAT_1:sch 1(A56, A42);
A58: j <= n by A17, FINSEQ_1:1;

per cases ( j < i + 1 or ( j > i + 1 & j < n ) or ( j > i + 1 & j = n ) ) by A18, A58, 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, A57, A19; :: thesis: verum

end;

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

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

end;

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

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

end;

end;