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

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