let m be non empty 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 FINSEQ_1:def 18;
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 A3: 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 A3, FINSEQ_2:8;

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

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

end;

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

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

end;

end;

end;

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