deffunc H₁( Element of N) -> Element of the carrier of R = "/\" ( { (N . k) where k is Element of N : k >= $1 } ,R);
consider g being Function of the carrier of N, the carrier of R such that
A1: for i being Element of N holds g . i = H₁(i) from FUNCT_2:sch 4();
reconsider f = g as Function of N,R ;
reconsider M = N *' f as strict prenet of R ;
take M ; :: thesis: ex f being Function of N,R st
( M = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) )
thus ex f being Function of N,R st
( M = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) by A1; :: thesis: verum