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 Tuple of m,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

let j be Nat; :: thesis: ( j in Seg m implies (2sComplement m,i) . j = a . j )
assume A2: j in Seg m ; :: thesis: (2sComplement m,i) . j = a . j
reconsider j = j as Nat ;
A3: ( len (2sComplement (m + 1),i) = m + 1 & len (2sComplement m,i) = m & len a = m ) by FINSEQ_1:def 18;
A4: ( 1 <= j & j <= m ) by A2, FINSEQ_1:3;
m <= m + 1 by NAT_1:11;
then j <= m + 1 by A4, XXREAL_0:2;
then A5: (2sComplement (m + 1),i) . j = (2sComplement (m + 1),i) /. j by A3, A4, FINSEQ_4:24
.= (2sComplement m,i) /. j by A4, Th32
.= (2sComplement m,i) . j by A3, A4, FINSEQ_4:24 ;
j in dom a by A2, A3, FINSEQ_1:def 3;
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 A6: m = 0 ; :: thesis: ex x being Element of BOOLEAN st 2sComplement (m + 1),i = (2sComplement m,i) ^ <*x*>

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

end;

end;

end;

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