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;