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)
then A2: i > len (0* j) by CARD_1:def 7;
0 > j - i by A1, XREAL_1:49;
then A3: j -' i = 0 by XREAL_0:def 2;
(0* j) /^ i = 0 by A2, RFINSEQ:def 1;
hence (0* j) /^ i = 0* (j -' i) by A3; :: thesis: verum