let n be Nat; :: thesis: Rev (0* n) = 0* n

A1: now :: thesis: for k being Nat st k in dom (0* n) holds
(Rev (0* n)) . k = (0* n) . k

let k be Nat; :: thesis: ( k in dom (0* n) implies (Rev (0* n)) . k = (0* n) . k )
assume A2: k in dom (0* n) ; :: thesis: (Rev (0* n)) . k = (0* n) . k
then k in Seg (len (0* n)) by FINSEQ_1:def 3;
then A3: k in Seg n by CARD_1:def 7;
then (n - k) + 1 in Seg n by FINSEQ_5:2;
then A4: ((len (0* n)) - k) + 1 in Seg n by CARD_1:def 7;
thus (Rev (0* n)) . k = (0* n) . (((len (0* n)) - k) + 1) by A2, FINSEQ_5:58
.= 0 by A4, FUNCOP_1:7
.= (0* n) . k by A3, FUNCOP_1:7 ; :: thesis: verum

end;

dom (Rev (0* n)) = Seg (len (Rev (0* n))) by FINSEQ_1:def 3
.= Seg (len (0* n)) by FINSEQ_5:def 3
.= dom (0* n) by FINSEQ_1:def 3 ;
hence Rev (0* n) = 0* n by A1, FINSEQ_1:13; :: thesis: verum