let I be non empty set ; :: thesis: for A being 1-sorted-yielding ManySortedSet of I

for L being ManySortedSubset of Carrier A

for i being Element of I

for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A

let A be 1-sorted-yielding ManySortedSet of I; :: thesis: for L being ManySortedSubset of Carrier A

for i being Element of I

for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A

let L be ManySortedSubset of Carrier A; :: thesis: for i being Element of I

for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A

let i be Element of I; :: thesis: for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A

let S be Subset of (A . i); :: thesis: L +* (i,S) is ManySortedSubset of Carrier A

A1: L c= Carrier A by PBOOLE:def 18;

A2: dom L = I by PARTFUN1:def 2;

L +* (i,S) c= Carrier A

for L being ManySortedSubset of Carrier A

for i being Element of I

for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A

let A be 1-sorted-yielding ManySortedSet of I; :: thesis: for L being ManySortedSubset of Carrier A

for i being Element of I

for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A

let L be ManySortedSubset of Carrier A; :: thesis: for i being Element of I

for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A

let i be Element of I; :: thesis: for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A

let S be Subset of (A . i); :: thesis: L +* (i,S) is ManySortedSubset of Carrier A

A1: L c= Carrier A by PBOOLE:def 18;

A2: dom L = I by PARTFUN1:def 2;

L +* (i,S) c= Carrier A

proof

hence
L +* (i,S) is ManySortedSubset of Carrier A
by PBOOLE:def 18; :: thesis: verum
let a be object ; :: according to PBOOLE:def 2 :: thesis: ( not a in I or (L +* (i,S)) . a c= (Carrier A) . a )

assume a in I ; :: thesis: (L +* (i,S)) . a c= (Carrier A) . a

then reconsider b = a as Element of I ;

end;assume a in I ; :: thesis: (L +* (i,S)) . a c= (Carrier A) . a

then reconsider b = a as Element of I ;