let n be Nat; :: thesis: for y being Tuple of n, BOOLEAN st y = 0* n holds
'not' y = n |-> 1
let y be Tuple of n, BOOLEAN ; :: thesis: ( y = 0* n implies 'not' y = n |-> 1 )
assume A1: y = 0* n ; :: thesis: 'not' y = n |-> 1

A2: now :: thesis: for i being Nat st 1 <= i & i <= len ('not' y) holds
('not' y) . i = (n |-> 1) . i

A3: len y = n by CARD_1:def 7;
let i be Nat; :: thesis: ( 1 <= i & i <= len ('not' y) implies ('not' y) . i = (n |-> 1) . i )
assume that
A4: 1 <= i and
A5: i <= len ('not' y) ; :: thesis: ('not' y) . i = (n |-> 1) . i
A6: len ('not' y) = n by CARD_1:def 7;
then A7: i in Seg n by A4, A5, FINSEQ_1:1;
then A8: y . i = FALSE by A1, FUNCOP_1:7;
thus ('not' y) . i = ('not' y) /. i by A4, A5, FINSEQ_4:15
.= 'not' (y /. i) by A7, BINARITH:def 1
.= 'not' FALSE by A4, A5, A6, A3, A8, FINSEQ_4:15
.= (n |-> 1) . i by A7, FUNCOP_1:7 ; :: thesis: verum

end;

len ('not' y) = n by CARD_1:def 7
.= len (n |-> 1) by CARD_1:def 7 ;
hence 'not' y = n |-> 1 by A2, FINSEQ_1:14; :: thesis: verum