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

.= 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

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

(Rev (0* n)) . k = (0* n) . k

dom (Rev (0* n)) =
Seg (len (Rev (0* n)))
by FINSEQ_1:def 3
(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;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

.= 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