let n be non zero Nat; :: thesis: for x, y being Tuple of n, BOOLEAN st x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds
for k being non zero Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )
let x, y be Tuple of n, BOOLEAN ; :: thesis: ( x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE implies for k being non zero Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE ) )
assume that
A1: x /. n = TRUE and
A2: (carry (x,(Bin1 n))) /. n = TRUE ; :: thesis: for k being non zero Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )
defpred S₁[ Nat] means ( $1 in Seg (n -' 1) implies ( x /. ((n -' $1) + 1) = TRUE & (carry (x,(Bin1 n))) /. ((n -' $1) + 1) = TRUE ) );
let k be non zero Nat; :: thesis: ( k <> 1 & k <= n implies ( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE ) )
assume that
A3: k <> 1 and
A4: k <= n ; :: thesis: ( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )
set i = (n -' k) + 1;
1 < k by A3, NAT_2:19;
then 1 + 1 <= k by NAT_1:13;
then A5: 1 <= k - 1 by XREAL_1:19;
A6: for j being non zero Nat st S₁[j] holds
S₁[j + 1]

proof

let j be non zero Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume that
A7: S₁[j] and
A8: j + 1 in Seg (n -' 1) ; :: thesis: ( x /. ((n -' (j + 1)) + 1) = TRUE & (carry (x,(Bin1 n))) /. ((n -' (j + 1)) + 1) = TRUE )
A9: j + 1 <= n -' 1 by A8, FINSEQ_1:1;
then A10: j < n -' 1 by NAT_1:13;
then j < n - 1 by NAT_1:14, XREAL_1:233;
then j + 1 < n by XREAL_1:20;
then A11: j < n by NAT_1:13;
j + 1 <= n - 1 by A9, NAT_1:14, XREAL_1:233;
then 1 <= (n - 1) - j by XREAL_1:19;
then 1 <= (n - j) - 1 ;
then 1 + 1 <= n - j by XREAL_1:19;
then 1 + 1 <= n -' j by A11, XREAL_1:233;
then A12: n -' j > 1 by NAT_1:13;
A13: 1 <= j by NAT_1:14;
A14: n -' j < n by NAT_2:9;
then n -' j in Seg n by A12, FINSEQ_1:1;
then A15: (Bin1 n) /. (n -' j) = FALSE by A12, BINARI_2:6;
then ((Bin1 n) /. (n -' j)) '&' ((carry (x,(Bin1 n))) /. (n -' j)) = FALSE ;
then A16: TRUE = ((x /. (n -' j)) '&' ((Bin1 n) /. (n -' j))) 'or' ((x /. (n -' j)) '&' ((carry (x,(Bin1 n))) /. (n -' j))) by A7, A13, A10, A14, A12, A15, BINARITH:def 2, FINSEQ_1:1
.= (x /. (n -' j)) '&' ((carry (x,(Bin1 n))) /. (n -' j)) by A15 ;
then x /. (n -' j) = TRUE by MARGREL1:12;
hence x /. ((n -' (j + 1)) + 1) = TRUE by A11, NAT_2:7; :: thesis: (carry (x,(Bin1 n))) /. ((n -' (j + 1)) + 1) = TRUE
(carry (x,(Bin1 n))) /. (n -' j) = TRUE by A16, MARGREL1:12;
hence (carry (x,(Bin1 n))) /. ((n -' (j + 1)) + 1) = TRUE by A11, NAT_2:7; :: thesis: verum

end;

A17: 1 <= (n -' k) + 1 by NAT_1:11;
(n -' k) + 1 = (n - k) + 1 by A4, XREAL_1:233
.= n - (k - 1) ;
then A18: (n -' k) + 1 <= n - 1 by A5, XREAL_1:13;
then ((n -' k) + 1) + 1 <= n by XREAL_1:19;
then (n -' k) + 1 < n by NAT_1:13;
then A19: k = (n -' ((n -' k) + 1)) + 1 by A4, NAT_2:5;
(n -' k) + 1 <= n -' 1 by A18, NAT_1:14, XREAL_1:233;
then A20: (n -' k) + 1 in Seg (n -' 1) by A17, FINSEQ_1:1;
A21: S₁[1] by A1, A2, NAT_1:14, XREAL_1:235;
for j being non zero Nat holds S₁[j] from NAT_1:sch 10(A21, A6);
hence ( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE ) by A19, A20; :: thesis: verum