let i, j be 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
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 A6: ((0* j) /^ i) . k = 0 ;
thus ((0* j) /^ i) . k = (0* (j -' i)) . k by A6; :: thesis: verum
end;
hence (0* j) /^ i = 0* (j -' i) by A2, A3; :: thesis: verum