let n be Nat; :: thesis: ( n < 10 implies Sierp36 n,n )
assume n < 10 ; :: thesis: Sierp36 n,n
then digits (n,10) = <%n%> by Th3;
hence Sum (digits (n,10)) = n by AFINSQ_2:53; :: according to NUMBER11:def 1 :: thesis: ( n divides n & ( for m being Nat st Sum (digits (m,10)) = n & n divides m holds
n <= m ) )
thus n divides n ; :: thesis: for m being Nat st Sum (digits (m,10)) = n & n divides m holds
n <= m

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: for m being Nat st Sum (digits (m,10)) = n & n divides m holds
n <= m

hence for m being Nat st Sum (digits (m,10)) = n & n divides m holds
n <= m ; :: thesis: verum

end;

suppose A1: n > 0 ; :: thesis: for m being Nat st Sum (digits (m,10)) = n & n divides m holds
n <= m

hereby :: thesis: verum

let m be Nat; :: thesis: ( Sum (digits (m,10)) = n & n divides m implies n <= m )
assume A2: ( Sum (digits (m,10)) = n & n divides m ) ; :: thesis: n <= m

now :: thesis: not m = 0

assume m = 0 ; :: thesis: contradiction
then digits (m,10) = <%0%> by Th3;
hence contradiction by A2, A1, AFINSQ_2:53; :: thesis: verum

end;

hence n <= m by A2, INT_2:27; :: thesis: verum

end;

end;

end;