let I be set ; :: thesis: for X being ManySortedSet of I
for S being ManySortedSubset of X
for x being object holds S . x is Subset of (X . x)
let X be ManySortedSet of I; :: thesis: for S being ManySortedSubset of X
for x being object holds S . x is Subset of (X . x)
let S be ManySortedSubset of X; :: thesis: for x being object holds S . x is Subset of (X . x)
let x be object ; :: thesis: S . x is Subset of (X . x)
A1: S c= X by PBOOLE:def 18;
( ( x in dom S & dom S = I ) or x nin dom S ) by PARTFUN1:def 2;
then ( S . x c= X . x or S . x = {} ) by A1, FUNCT_1:def 2;
hence S . x is Subset of (X . x) by XBOOLE_1:2; :: thesis: verum