defpred S₁[ set ] means ex g being natural-valued ManySortedSet of X st
( $1 = g & ( for x being set st x in X holds
g . x <= f . x ) );
consider IT being Subset of (Funcs (X,NAT)) such that
A1: for h being set holds
( h in IT iff ( h in Funcs (X,NAT) & S₁[h] ) ) from SUBSET_1:sch 1();
take IT ; :: thesis: for g being natural-valued ManySortedSet of X holds
( g in IT iff for x being set st x in X holds
g . x <= f . x )
let g be natural-valued ManySortedSet of X; :: thesis: ( g in IT iff for x being set st x in X holds
g . x <= f . x )
( dom g = X & rng g c= NAT ) by PARTFUN1:def 2, VALUED_0:def 6;
then g is Function of X,NAT by RELSET_1:4;
then A2: g in Funcs (X,NAT) by FUNCT_2:8;
assume for x being set st x in X holds
g . x <= f . x ; :: thesis: g in IT
hence g in IT by A1, A2; :: thesis: verum