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:117;
now :: thesis: ex x being Element of BOOLEAN st 2sComplement ((m + 1),i) = (2sComplement (m,i)) ^ <*x*>
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 zero 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 CARD_1:def 7;
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:1;
len a = m by CARD_1:def 7;
then A5: j in dom a by A3, FINSEQ_1:def 3;
A6: j <= m by A3, FINSEQ_1:1;
m <= m + 1 by NAT_1:11;
then ( len (2sComplement ((m + 1),i)) = m + 1 & j <= m + 1 ) by A6, CARD_1:def 7, XXREAL_0:2;
then (2sComplement ((m + 1),i)) . j = (2sComplement ((m + 1),i)) /. j by A4, FINSEQ_4:15
.= (2sComplement (m,i)) /. j by A4, A6, Th32
.= (2sComplement (m,i)) . j by A2, A4, A6, FINSEQ_4:15 ;
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:119;
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:97;
A9: 2sComplement ((m + 1),i) = {} ^ <*c*> by A8, FINSEQ_1:34;
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