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 :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

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

now :: thesis: ( i < n + 1 implies H₁(n + 1) . (i + 1) = TRUE )

assume A4: i < n + 1 ; :: thesis: H₁(n + 1) . (i + 1) = TRUE
then A5: i <= n by NAT_1:13;
A6: n in NAT by ORDINAL1:def 12;

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

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

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

end;

suppose A11: ( 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 ;
then A12: len (0* n) = n by FINSEQ_1:def 3, A6;
dom <*TRUE*> = Seg 1 by FINSEQ_1:38;
then A13: 1 in dom <*TRUE*> by FINSEQ_1:1;
thus H₁(n + 1) . (i + 1) = ((0* n) ^ <*TRUE*>) . (i + 1) by A11, BINARI_3:28
.= <*TRUE*> . 1 by A11, A12, A13, FINSEQ_1:def 7
.= TRUE by FINSEQ_1:40 ; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

A17: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A17, 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₂[ 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
A18: j in Seg n and
A19: j <> i + 1 ; :: thesis: (n -BinarySequence (2 to_power i)) . j = 0
A20: 1 <= j by A18, FINSEQ_1:1;

A21: now :: thesis: for n being Nat st S₂[n] holds
S₂[n + 1]

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A22: S₂[n] ; :: thesis: S₂[n + 1]

now :: thesis: ( i < n + 1 implies for j being Element of NAT st i + 1 <= j & j <= n + 1 holds
H₁(n + 1) . (j + 1) = FALSE )

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 A23: i <= n by NAT_1:13;
A24: 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
A25: i + 1 <= j and
A26: 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 A23, XXREAL_0:1;

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

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

end;

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

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

end;

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

then reconsider n9 = n as non zero Nat ;
A32: 2 to_power i < 2 to_power n by A31, POWER:39;
thus H₁(n + 1) . (j + 1) = FALSE :: thesis: verum

proof

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

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

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

then A34: 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 A34, FINSEQ_1:1;
hence H₁(n + 1) . (j + 1) = FALSE by FUNCT_1:def 2; :: thesis: verum

end;

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

dom H₁(n) = Seg n by Lm1;
then A36: j = len H₁(n) by A35, FINSEQ_1:def 3;
dom <*FALSE*> = Seg 1 by FINSEQ_1:38;
then A37: 1 in dom <*FALSE*> by FINSEQ_1:1;
thus H₁(n + 1) . (j + 1) = (H₁(n9) ^ <*FALSE*>) . (j + 1) by A32, BINARI_3:27
.= <*FALSE*> . 1 by A36, A37, FINSEQ_1:def 7
.= FALSE by FINSEQ_1:40 ; :: thesis: verum

end;

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

A39: 1 <= j + 1 by NAT_1:12;
j + 1 <= n by A38, NAT_1:13;
then j + 1 in Seg n by A39, FINSEQ_1:1;
then A40: j + 1 in dom H₁(n) by Lm1;
thus H₁(n + 1) . (j + 1) = (H₁(n9) ^ <*FALSE*>) . (j + 1) by A32, BINARI_3:27
.= H₁(n) . (j + 1) by A40, FINSEQ_1:def 7
.= FALSE by A22, A25, A31, A38 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

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

end;

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

A43: now :: thesis: for n being Nat st S₃[n] holds
S₃[n + 1]

let n be Nat; :: thesis: ( S₃[n] implies S₃[n + 1] )
assume A44: S₃[n] ; :: thesis: S₃[n + 1]

now :: thesis: ( i < n + 1 implies for j being Element of NAT st 1 <= j & j < i + 1 holds
H₁(n + 1) . j = FALSE )

assume A45: i < n + 1 ; :: thesis: for j being Element of NAT st 1 <= j & j < i + 1 holds
H₁(n + 1) . b₂ = FALSE
then A46: 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
A47: 1 <= j and
A48: j < i + 1 ; :: thesis: H₁(n + 1) . b₁ = FALSE

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 A45, NAT_1:13;
hence H₁(n + 1) . j = FALSE by A47, A48; :: thesis: verum

end;

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

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

end;

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

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

end;

end;

end;

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

end;

A57: S₃[ 0 ] ;
A58: for n being Nat holds S₃[n] from NAT_1:sch 2(A57, A43);
A59: j <= n by A18, FINSEQ_1:1;

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

end;

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

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

end;

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

then consider m being Nat such that
A64: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
i < m by A63, A64, 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 A63, A64, BINARI_3:26; :: thesis: verum

end;

end;