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 )

hereby :: thesis: ( ( for x being set st x in X holds
g . x <= f . x ) implies g in IT )

assume g in IT ; :: thesis: for x being set st x in X holds
g . x <= f . x
then ex g1 being natural-valued ManySortedSet of X st
( g1 = g & ( for x being set st x in X holds
g1 . x <= f . x ) ) by A1;
hence for x being set st x in X holds
g . x <= f . x ; :: thesis: verum

end;

( dom g = X & rng g c= NAT ) by PARTFUN1:def 2;
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