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 by FINSEQ_1:def 18;
A2: 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 A6: 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 A6, BINARITH:3 ;
hence ('not' (z ^ <*d*>)) /. i = (('not' z) ^ <*('not' d)*>) /. i by A6, BINARITH:3; :: thesis: verum

end;

end;

end;

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