let i, j be Nat; :: thesis: (0* j) /^ i = 0* (j -' i)
per cases ( i <= j or i > j ) ;
suppose i <= j ; :: thesis: (0* j) /^ i = 0* (j -' i)
hence (0* j) /^ i = 0* (j -' i) by Lm3; :: thesis: verum
end;
suppose i > j ; :: thesis: (0* j) /^ i = 0* (j -' i)
hence (0* j) /^ i = 0* (j -' i) by Lm4; :: thesis: verum
end;
end;