let y, z be Tuple of n, BOOLEAN ; :: thesis: ( ( for i being Nat st i in Seg n holds
y /. i = 'not' (x /. i) ) & ( for i being Nat st i in Seg n holds
z /. i = 'not' (x /. i) ) implies y = z )
assume that
A5: for i being Nat st i in Seg n holds
y /. i = 'not' (x /. i) and
A6: for i being Nat st i in Seg n holds
z /. i = 'not' (x /. i) ; :: thesis: y = z
A7: len y = n by CARD_1:def 7;
then A8: dom y = Seg n by FINSEQ_1:def 3;
A9: len z = n by CARD_1:def 7;

now :: thesis: for j being Nat st j in dom y holds
y . j = z . j

let j be Nat; :: thesis: ( j in dom y implies y . j = z . j )
assume A10: j in dom y ; :: thesis: y . j = z . j
then A11: j in dom z by A9, A8, FINSEQ_1:def 3;
thus y . j = y /. j by A10, PARTFUN1:def 6
.= 'not' (x /. j) by A5, A8, A10
.= z /. j by A6, A8, A10
.= z . j by A11, PARTFUN1:def 6 ; :: thesis: verum

end;

hence y = z by A7, A9, FINSEQ_2:9; :: thesis: verum