let I be non empty set ; :: thesis: for A being 1-sorted-yielding ManySortedSet of
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 ; :: 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: dom L = I by PARTFUN1:def 4;
A2: L c= Carrier A by PBOOLE:def 23;
L +* i,S c= Carrier A

proof

let a be set ; :: according to PBOOLE:def 5 :: 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 ;

per cases ( a = i or a <> i ) ;

suppose A3: a = i ; :: thesis: (L +* i,S) . a c= (Carrier A) . a

then (L +* i,S) . b = S by A1, FUNCT_7:33;
then (L +* i,S) . b c= the carrier of (A . b) by A3;
hence (L +* i,S) . a c= (Carrier A) . a by YELLOW_6:9; :: thesis: verum

end;

suppose a <> i ; :: thesis: (L +* i,S) . a c= (Carrier A) . a

then (L +* i,S) . a = L . b by FUNCT_7:34;
hence (L +* i,S) . a c= (Carrier A) . a by A2, PBOOLE:def 5; :: thesis: verum

end;

end;

end;

hence L +* i,S is ManySortedSubset of Carrier A by PBOOLE:def 23; :: thesis: verum