let m be non zero Nat; :: thesis: for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds 'not' (z ^ <*d*>) = ('not' z) ^ <*('not' d)*>
let z be Tuple of m, BOOLEAN ; :: thesis: for d being Element of BOOLEAN holds 'not' (z ^ <*d*>) = ('not' z) ^ <*('not' d)*>
let d be Element of BOOLEAN ; :: thesis: 'not' (z ^ <*d*>) = ('not' z) ^ <*('not' d)*>
A1: ( len ('not' (z ^ <*d*>)) = m + 1 & len (('not' z) ^ <*('not' d)*>) = m + 1 ) by CARD_1:def 7;
for i being Nat st i in Seg (m + 1) holds
('not' (z ^ <*d*>)) /. i = (('not' z) ^ <*('not' d)*>) /. i

proof

let i be Nat; :: thesis: ( i in Seg (m + 1) implies ('not' (z ^ <*d*>)) /. i = (('not' z) ^ <*('not' d)*>) /. i )
assume A2: i in Seg (m + 1) ; :: thesis: ('not' (z ^ <*d*>)) /. i = (('not' z) ^ <*('not' d)*>) /. i

per cases ( i in Seg m or i = m + 1 ) by A2, FINSEQ_2:7;

suppose A3: i in Seg m ; :: thesis: ('not' (z ^ <*d*>)) /. i = (('not' z) ^ <*('not' d)*>) /. i

A4: ('not' (z ^ <*d*>)) /. i = 'not' ((z ^ <*d*>) /. i) by A2, BINARITH:def 1
.= 'not' (z /. i) by A3, BINARITH:1 ;
(('not' z) ^ <*('not' d)*>) /. i = ('not' z) /. i by A3, BINARITH:1
.= 'not' (z /. i) by A3, BINARITH:def 1 ;
hence ('not' (z ^ <*d*>)) /. i = (('not' z) ^ <*('not' d)*>) /. i by A4; :: thesis: verum

end;

suppose A5: i = m + 1 ; :: thesis: ('not' (z ^ <*d*>)) /. i = (('not' z) ^ <*('not' d)*>) /. i

('not' (z ^ <*d*>)) /. i = 'not' ((z ^ <*d*>) /. i) by A2, BINARITH:def 1
.= 'not' d by A5, BINARITH:2 ;
hence ('not' (z ^ <*d*>)) /. i = (('not' z) ^ <*('not' d)*>) /. i by A5, BINARITH:2; :: thesis: verum

end;

end;

end;

hence 'not' (z ^ <*d*>) = ('not' z) ^ <*('not' d)*> by A1, Lm1; :: thesis: verum