let i, j be Nat; :: thesis: ( i <= j implies (0* j) | i = 0* i )
assume A1: i <= j ; :: thesis: (0* j) | i = 0* i
A2: ((0* i) ^ (0* (j -' i))) | (len (0* i)) = 0* i by FINSEQ_5:23;
i + (j -' i) = (i + j) -' i by A1, Lm2;
then i + (j -' i) = (i + j) - i by XREAL_0:def 2;
then (0* i) ^ (0* (j -' i)) = 0* j by FINSEQ_2:123;
hence (0* j) | i = 0* i by A2, CARD_1:def 7; :: thesis: verum