let n, m, l be natural Ordinal; :: thesis: ( n divides m & n divides m +^ l implies n divides l )
assume n divides m ; :: thesis: ( not n divides m +^ l or n divides l )
then consider a being natural Ordinal such that
A1: m = n *^ a by Th5;
assume n divides m +^ l ; :: thesis: n divides l
then consider b being natural Ordinal such that
A2: m +^ l = n *^ b by Th5;
assume A3: not n divides l ; :: thesis: contradiction
l = (n *^ b) -^ (n *^ a) by A1, A2, ORDINAL3:52
.= (b -^ a) *^ n by ORDINAL3:63 ;
hence contradiction by A3; :: thesis: verum