let n, i be Element of NAT ; :: thesis: (0* n) /^ i = 0* (n -' i)
A1: n = len (0* n) by FINSEQ_1:def 18;
A2: len ((0* n) /^ i) = (len (0* n)) -' i by JORDAN3:19
.= n -' i by FINSEQ_1:def 18 ;
A3: n -' i = len (0* (n -' i)) by FINSEQ_1:def 18;
for j being Nat st 1 <= j & j <= n -' i holds
((0* n) /^ i) . j = (0* (n -' i)) . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= n -' i implies ((0* n) /^ i) . j = (0* (n -' i)) . j )
assume A4: ( 1 <= j & j <= n -' i ) ; :: thesis: ((0* n) /^ i) . j = (0* (n -' i)) . j
then A5: j in Seg (n -' i) by FINSEQ_1:3;
then A6: j in dom ((0* n) /^ i) by A2, FINSEQ_1:def 3;

now

assume n < i ; :: thesis: contradiction
then n - i < i - i by XREAL_1:11;
hence contradiction by A4, XREAL_0:def 2; :: thesis: verum

end;

then n -' i = n - i by XREAL_1:235;
then A7: j + i <= (n - i) + i by A4, XREAL_1:8;
1 <= j + i by A4, NAT_1:12;
then A8: j + i in Seg n by A7, FINSEQ_1:3;

now

per cases ( i <= len (0* n) or i > len (0* n) ) ;

case i <= len (0* n) ; :: thesis: ((0* n) /^ i) . j = (0* (n -' i)) . j

hence ((0* n) /^ i) . j = (n |-> 0 ) . (j + i) by A6, RFINSEQ:def 2
.= 0 by A8, FUNCOP_1:13
.= (0* (n -' i)) . j by A5, FUNCOP_1:13 ;
:: thesis: verum

end;

case A9: i > len (0* n) ; :: thesis: ((0* n) /^ i) . j = (0* (n -' i)) . j

then i - i > n - i by A1, XREAL_1:11;
then A10: n -' i = 0 by XREAL_0:def 2;
((0* n) /^ i) . j = (<*> REAL ) . j by A9, RFINSEQ:def 2;
hence ((0* n) /^ i) . j = (0* (n -' i)) . j by A10, FINSEQ_2:72; :: thesis: verum

end;

end;

end;

hence ((0* n) /^ i) . j = (0* (n -' i)) . j ; :: thesis: verum

end;

hence (0* n) /^ i = 0* (n -' i) by A2, A3, FINSEQ_1:18; :: thesis: verum