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
proof
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 ;
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 A2, FUNCT_7:31;
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:2; :: 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:32;
hence (L +* (i,S)) . a c= (Carrier A) . a by A1; :: thesis: verum
end;
end;
end;
hence L +* (i,S) is ManySortedSubset of Carrier A by PBOOLE:def 18; :: thesis: verum