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: len ('not' y) = n by FINSEQ_1:def 18
.= len (n |-> 1) by FINSEQ_1:def 18 ;

now

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

end;

hence 'not' y = n |-> 1 by A2, FINSEQ_1:18; :: thesis: verum