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;

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

hence
y = z
by A7, A9, FINSEQ_2:9; :: thesis: verumy . 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;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