take N ; :: thesis: ex f being Function of N,N st
( the mapping of N = the mapping of N * f & ( for m being Element of N ex n being Element of N st
for p being Element of N st n <= p holds
m <= f . p ) )
take id N ; :: thesis: ( the mapping of N = the mapping of N * (id N) & ( for m being Element of N ex n being Element of N st
for p being Element of N st n <= p holds
m <= (id N) . p ) )
thus the mapping of N = the mapping of N * (id N) by FUNCT_2:17; :: thesis: for m being Element of N ex n being Element of N st
for p being Element of N st n <= p holds
m <= (id N) . p
let m be Element of N; :: thesis: ex n being Element of N st
for p being Element of N st n <= p holds
m <= (id N) . p
take n = m; :: thesis: for p being Element of N st n <= p holds
m <= (id N) . p
let p be Element of N; :: thesis: ( n <= p implies m <= (id N) . p )
assume n <= p ; :: thesis: m <= (id N) . p
hence m <= (id N) . p ; :: thesis: verum