let i, j be Element of NAT ; :: thesis: ( i <= j implies (0* j) /^ i = 0* (j -' i) )
assume A1: i <= j ; :: thesis: (0* j) /^ i = 0* (j -' i)
len ((0* j) /^ i) = (len (0* j)) -' i by RFINSEQ:29;
then A2: len ((0* j) /^ i) = j -' i by CARD_1:def 7;
A3: len (0* (j -' i)) = j -' i by CARD_1:def 7;
A4: i <= len (0* j) by A1, CARD_1:def 7;
for k being Nat st 1 <= k & k <= len ((0* j) /^ i) holds
((0* j) /^ i) . k = (0* (j -' i)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len ((0* j) /^ i) implies ((0* j) /^ i) . k = (0* (j -' i)) . k )
assume A5: ( 1 <= k & k <= len ((0* j) /^ i) ) ; :: thesis: ((0* j) /^ i) . k = (0* (j -' i)) . k
then k <= j - i by A2, XREAL_0:def 2;
then A6: k + i <= j by XREAL_1:19;
1 <= k + i by A5, XREAL_1:38;
then A7: k + i in Seg j by A6;
k in dom ((0* j) /^ i) by A5, FINSEQ_3:25;
then ((0* j) /^ i) . k = (0* j) . (k + i) by A4, RFINSEQ:def 1;
then A8: ((0* j) /^ i) . k = 0 by A7, FINSEQ_2:57;
k in Seg (j -' i) by A5, A2, FINSEQ_1:1;
hence ((0* j) /^ i) . k = (0* (j -' i)) . k by A8, FINSEQ_2:57; :: thesis: verum

end;

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