let I be set ; :: thesis: for M being ManySortedSet of
for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
let M be ManySortedSet of ; :: thesis: for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
let A, B be SubsetFamily of M; :: thesis: MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
reconsider MAB = MSUnion (A \/ B) as ManySortedSubset of M ;
reconsider MAB = MAB as ManySortedSet of ;
reconsider MA = MSUnion A as ManySortedSubset of M ;
reconsider MA = MA as ManySortedSet of ;
reconsider MB = MSUnion B as ManySortedSubset of M ;
reconsider MB = MB as ManySortedSet of ;
for i being set st i in I holds
MAB . i = (MA \/ MB) . i

proof

let i be set ; :: thesis: ( i in I implies MAB . i = (MA \/ MB) . i )
assume A1: i in I ; :: thesis: MAB . i = (MA \/ MB) . i
then A2: MAB . i = union { (f . i) where f is Element of Bool M : f in A \/ B } by Def4;
A3: (MA \/ MB) . i = (MA . i) \/ (MB . i) by A1, PBOOLE:def 7;
A4: MA . i = union { (f . i) where f is Element of Bool M : f in A } by A1, Def4;
A5: MB . i = union { (f . i) where f is Element of Bool M : f in B } by A1, Def4;
A6: for v being set st v in MAB . i holds
v in (MA \/ MB) . i

proof

let v be set ; :: thesis: ( v in MAB . i implies v in (MA \/ MB) . i )
assume v in MAB . i ; :: thesis: v in (MA \/ MB) . i
then consider h being set such that
A7: v in h and
A8: h in { (f . i) where f is Element of Bool M : f in A \/ B } by A2, TARSKI:def 4;
consider g being Element of Bool M such that
A9: h = g . i and
A10: g in A \/ B by A8;
( g in A or g in B ) by A10, XBOOLE_0:def 3;
then ( h in { (f . i) where f is Element of Bool M : f in A } or h in { (f . i) where f is Element of Bool M : f in B } ) by A9;
then ( v in union { (f . i) where f is Element of Bool M : f in A } or v in union { (f . i) where f is Element of Bool M : f in B } ) by A7, TARSKI:def 4;
hence v in (MA \/ MB) . i by A3, A4, A5, XBOOLE_0:def 3; :: thesis: verum

end;

for v being set st v in (MA \/ MB) . i holds
v in MAB . i

proof

let v be set ; :: thesis: ( v in (MA \/ MB) . i implies v in MAB . i )
assume v in (MA \/ MB) . i ; :: thesis: v in MAB . i
then A11: ( v in MA . i or v in MB . i ) by A3, XBOOLE_0:def 3;

per cases ( v in union { (f . i) where f is Element of Bool M : f in A } or v in union { (f . i) where f is Element of Bool M : f in B } ) by A1, A11, Def4;

suppose v in union { (f . i) where f is Element of Bool M : f in A } ; :: thesis: v in MAB . i

then consider g being set such that
A12: v in g and
A13: g in { (f . i) where f is Element of Bool M : f in A } by TARSKI:def 4;
consider h being Element of Bool M such that
A14: g = h . i and
A15: h in A by A13;
h in A \/ B by A15, XBOOLE_0:def 3;
then g in { (f . i) where f is Element of Bool M : f in A \/ B } by A14;
hence v in MAB . i by A2, A12, TARSKI:def 4; :: thesis: verum

end;

suppose v in union { (f . i) where f is Element of Bool M : f in B } ; :: thesis: v in MAB . i

then consider g being set such that
A16: v in g and
A17: g in { (f . i) where f is Element of Bool M : f in B } by TARSKI:def 4;
consider h being Element of Bool M such that
A18: g = h . i and
A19: h in B by A17;
h in A \/ B by A19, XBOOLE_0:def 3;
then g in { (f . i) where f is Element of Bool M : f in A \/ B } by A18;
hence v in MAB . i by A2, A16, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence MAB . i = (MA \/ MB) . i by A6, TARSKI:2; :: thesis: verum

end;

hence MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B) by PBOOLE:3; :: thesis: verum