let it1, it2 be Subset of (Funcs (X,NAT)); :: thesis: ( ( for g being natural-valued ManySortedSet of X holds
( g in it1 iff for x being set st x in X holds
g . x <= f . x ) ) & ( for g being natural-valued ManySortedSet of X holds
( g in it2 iff for x being set st x in X holds
g . x <= f . x ) ) implies it1 = it2 )
assume that
A3: for g being natural-valued ManySortedSet of X holds
( g in it1 iff for x being set st x in X holds
g . x <= f . x ) and
A4: for g being natural-valued ManySortedSet of X holds
( g in it2 iff for x being set st x in X holds
g . x <= f . x ) ; :: thesis: it1 = it2
now :: thesis: for h being Element of Funcs (X,NAT) holds
( ( h in it1 implies h in it2 ) & ( h in it2 implies h in it1 ) )
let h be Element of Funcs (X,NAT); :: thesis: ( ( h in it1 implies h in it2 ) & ( h in it2 implies h in it1 ) )
hereby :: thesis: ( h in it2 implies h in it1 )
assume h in it1 ; :: thesis: h in it2
then for x being set st x in X holds
h . x <= f . x by A3;
hence h in it2 by A4; :: thesis: verum
end;
assume h in it2 ; :: thesis: h in it1
then for x being set st x in X holds
h . x <= f . x by A4;
hence h in it1 by A3; :: thesis: verum
end;
hence it1 = it2 by SUBSET_1:3; :: thesis: verum