let m be Nat; :: thesis: for i being Integer ex x being Element of BOOLEAN st 2sComplement (m + 1),i = (2sComplement m,i) ^ <*x*>
let i be Integer; :: thesis: ex x being Element of BOOLEAN st 2sComplement (m + 1),i = (2sComplement m,i) ^ <*x*>
consider a being Element of m -tuples_on BOOLEAN , b being Element of BOOLEAN such that
A1: 2sComplement (m + 1),i = a ^ <*b*> by FINSEQ_2:137;

now

per cases ( m > 0 or m = 0 ) ;

suppose m > 0 ; :: thesis: ex x being Element of BOOLEAN st 2sComplement (m + 1),i = (2sComplement m,i) ^ <*x*>

then reconsider m = m as non empty Nat ;
for j being Nat st j in Seg m holds
(2sComplement m,i) . j = a . j

proof

A2: len (2sComplement m,i) = m by FINSEQ_1:def 18;
let j be Nat; :: thesis: ( j in Seg m implies (2sComplement m,i) . j = a . j )
assume A3: j in Seg m ; :: thesis: (2sComplement m,i) . j = a . j
reconsider j = j as Nat ;
A4: 1 <= j by A3, FINSEQ_1:3;
len a = m by FINSEQ_1:def 18;
then A5: j in dom a by A3, FINSEQ_1:def 3;
A6: j <= m by A3, FINSEQ_1:3;
m <= m + 1 by NAT_1:11;
then ( len (2sComplement (m + 1),i) = m + 1 & j <= m + 1 ) by A6, FINSEQ_1:def 18, XXREAL_0:2;
then (2sComplement (m + 1),i) . j = (2sComplement (m + 1),i) /. j by A4, FINSEQ_4:24
.= (2sComplement m,i) /. j by A4, A6, Th32
.= (2sComplement m,i) . j by A2, A4, A6, FINSEQ_4:24 ;
hence (2sComplement m,i) . j = a . j by A1, A5, FINSEQ_1:def 7; :: thesis: verum

end;

then a = 2sComplement m,i by FINSEQ_2:139;
hence ex x being Element of BOOLEAN st 2sComplement (m + 1),i = (2sComplement m,i) ^ <*x*> by A1; :: thesis: verum

end;

suppose A7: m = 0 ; :: thesis: ex x being Element of BOOLEAN st 2sComplement (m + 1),i = (2sComplement m,i) ^ <*x*>

then consider c being Element of BOOLEAN such that
A8: 2sComplement (m + 1),i = <*c*> by FINSEQ_2:117;
A9: 2sComplement (m + 1),i = {} ^ <*c*> by A8, FINSEQ_1:47;
2sComplement m,i = {} by A7;
hence ex x being Element of BOOLEAN st 2sComplement (m + 1),i = (2sComplement m,i) ^ <*x*> by A9; :: thesis: verum

end;

end;

end;

hence ex x being Element of BOOLEAN st 2sComplement (m + 1),i = (2sComplement m,i) ^ <*x*> ; :: thesis: verum