let n be non zero Nat; :: thesis: for x being Tuple of n, BOOLEAN
for m, l being Nat
for y being Tuple of l, BOOLEAN st y = x ^ (0* m) holds
Absval y = Absval x
let x be Tuple of n, BOOLEAN ; :: thesis: for m, l being Nat
for y being Tuple of l, BOOLEAN st y = x ^ (0* m) holds
Absval y = Absval x
defpred S₁[ Nat] means for l being Nat
for y being Tuple of l, BOOLEAN st y = x ^ (0* $1) holds
Absval y = Absval x;
A1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: for l being Nat
for y being Tuple of l, BOOLEAN st y = x ^ (0* m) holds
Absval y = Absval x ; :: thesis: S₁[m + 1]
let l be Nat; :: thesis: for y being Tuple of l, BOOLEAN st y = x ^ (0* (m + 1)) holds
Absval y = Absval x
let y be Tuple of l, BOOLEAN ; :: thesis: ( y = x ^ (0* (m + 1)) implies Absval y = Absval x )
assume A3: y = x ^ (0* (m + 1)) ; :: thesis: Absval y = Absval x
0* m in BOOLEAN * by BINARI_3:4;
then reconsider z = 0* m as Tuple of m, BOOLEAN by FINSEQ_1:def 11;
x ^ z is Tuple of n + m, BOOLEAN ;
then reconsider y1 = x ^ (0* m) as Tuple of n + m, BOOLEAN ;
0* (m + 1) = (0* m) ^ <*FALSE*> by FINSEQ_2:60;
then A4: y = y1 ^ <*FALSE*> by FINSEQ_1:32, A3;
X1: len y = l by CARD_1:def 7;
len (y1 ^ <*FALSE*>) = (len y1) + (len <*FALSE*>) by FINSEQ_1:22
.= (len y1) + 1 by FINSEQ_1:40
.= (n + m) + 1 by CARD_1:def 7 ;
hence Absval y = (Absval y1) + (IFEQ (FALSE,FALSE,0,(2 to_power (n + m)))) by X1, BINARITH:20, A4
.= (Absval x) + (IFEQ (FALSE,FALSE,0,(2 to_power (n + m)))) by A2
.= (Absval x) + 0 by FUNCOP_1:def 8
.= Absval x ;
:: thesis: verum

end;

A0: S₁[ 0 ]

proof

let l be Nat; :: thesis: for y being Tuple of l, BOOLEAN st y = x ^ (0* 0) holds
Absval y = Absval x
let y be Tuple of l, BOOLEAN ; :: thesis: ( y = x ^ (0* 0) implies Absval y = Absval x )
assume AS2: y = x ^ (0* 0) ; :: thesis: Absval y = Absval x
A3: x ^ (0* 0) = x by FINSEQ_1:34;
x is Tuple of l, BOOLEAN by FINSEQ_1:34, AS2;
then len x = l by CARD_1:def 7;
hence Absval y = Absval x by A3, AS2, CARD_1:def 7; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A0, A1);
hence for m, l being Nat
for y being Tuple of l, BOOLEAN st y = x ^ (0* m) holds
Absval y = Absval x ; :: thesis: verum