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: 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 ;

now

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 FINSEQ_1:def 18;
then (n - k) + 1 in Seg n by FINSEQ_5:2;
then A5: ((len ('not' y)) - k) + 1 in Seg n by FINSEQ_1:def 18;
thus (Rev ('not' y)) . k = ('not' y) . (((len ('not' y)) - k) + 1) by A3, FINSEQ_5:61
.= (n |-> 1) . (((len ('not' y)) - k) + 1) by A1, Th6
.= 1 by A5, FUNCOP_1:13
.= (n |-> 1) . k by A4, FUNCOP_1:13
.= ('not' y) . k by A1, Th6 ; :: thesis: verum

end;

hence Rev ('not' y) = 'not' y by A2, FINSEQ_1:17; :: thesis: verum