let a, b be natural Ordinal; :: thesis:
thus ( a divides b implies ex c being natural Ordinal st b = a *^ c ) :: thesis:

given c being Ordinal such that A1: b = a *^ c ; :: according to ARYTM_3:def 3 :: thesis:

suppose b = {} ; :: thesis:

then b = a *^ {} by ORDINAL2:38;
hence ex c being natural Ordinal st b = a *^ c ; :: thesis:

end;

suppose b <> {} ; :: thesis:

then c is Element of omega by A1, ORDINAL3:75;
hence ex c being natural Ordinal st b = a *^ c by A1; :: thesis:

end;

end;

end;

thus ( ex c being natural Ordinal st b = a *^ c implies a divides b ) ; :: thesis: