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

A2: now :: thesis: for k being Nat st k in dom ('not' y) holds
(Rev ('not' y)) . k = ('not' y) . k

let k be Nat; :: thesis: ( k in dom ('not' y) implies (Rev ('not' y)) . k = ('not' y) . k )
assume A3: k in dom ('not' y) ; :: thesis: (Rev ('not' y)) . k = ('not' y) . k
then k in Seg (len ('not' y)) by FINSEQ_1:def 3;
then A4: k in Seg n by CARD_1:def 7;
then (n - k) + 1 in Seg n by FINSEQ_5:2;
then A5: ((len ('not' y)) - k) + 1 in Seg n by CARD_1:def 7;
thus (Rev ('not' y)) . k = ('not' y) . (((len ('not' y)) - k) + 1) by A3, FINSEQ_5:58
.= (n |-> 1) . (((len ('not' y)) - k) + 1) by A1, Th5
.= 1 by A5, FUNCOP_1:7
.= (n |-> 1) . k by A4, FUNCOP_1:7
.= ('not' y) . k by A1, Th5 ; :: thesis: verum

end;

dom (Rev ('not' y)) = Seg (len (Rev ('not' y))) by FINSEQ_1:def 3
.= Seg (len ('not' y)) by FINSEQ_5:def 3
.= dom ('not' y) by FINSEQ_1:def 3 ;
hence Rev ('not' y) = 'not' y by A2, FINSEQ_1:13; :: thesis: verum