let n, i be Element of NAT ; :: thesis: (0* n) /^ i = 0* (n -' i)
A1: len ((0* n) /^ i) = (len (0* n)) -' i by RFINSEQ:29
.= n -' i by CARD_1:def 7 ;
A2: n = len (0* n) by CARD_1:def 7;
A3: 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 that
A4: 1 <= j and
A5: j <= n -' i ; :: thesis: ((0* n) /^ i) . j = (0* (n -' i)) . j

now :: thesis: not n < i

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

end;

then n -' i = n - i by XREAL_1:233;
then A6: j + i <= (n - i) + i by A5, XREAL_1:6;
1 <= j + i by A4, NAT_1:12;
then A7: j + i in Seg n by A6, FINSEQ_1:1;
A8: j in Seg (n -' i) by A4, A5, FINSEQ_1:1;
then A9: j in dom ((0* n) /^ i) by A1, FINSEQ_1:def 3;

now :: thesis: ( ( i <= len (0* n) & ((0* n) /^ i) . j = (0* (n -' i)) . j ) or ( i > len (0* n) & ((0* n) /^ i) . j = (0* (n -' i)) . j ) )

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 A9, RFINSEQ:def 1
.= 0 by A7, FUNCOP_1:7
.= (0* (n -' i)) . j by A8, FUNCOP_1:7 ;
:: thesis: verum

end;

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

then i - i > n - i by A2, XREAL_1:9;
then A11: n -' i = 0 by XREAL_0:def 2;
((0* n) /^ i) . j = (<*> REAL) . j by A10, RFINSEQ:def 1;
hence ((0* n) /^ i) . j = (0* (n -' i)) . j by A11; :: thesis: verum

end;

end;

end;

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

end;

n -' i = len (0* (n -' i)) by CARD_1:def 7;
hence (0* n) /^ i = 0* (n -' i) by A1, A3, FINSEQ_1:14; :: thesis: verum