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

proof

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

per cases ( b = {} or b <> {} ) ;

suppose b = {} ; :: thesis: ex c being natural Ordinal st b = a *^ c

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

end;

suppose b <> {} ; :: thesis: ex c being natural Ordinal st b = a *^ c

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

end;

end;

end;

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