let I be set ; :: thesis: for M being ManySortedSet of I

for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) (\/) (MSUnion B)

let M be ManySortedSet of I; :: 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 I ;

reconsider MA = MSUnion A as ManySortedSubset of M ;

reconsider MA = MA as ManySortedSet of I ;

reconsider MB = MSUnion B as ManySortedSubset of M ;

reconsider MB = MB as ManySortedSet of I ;

for i being object st i in I holds

MAB . i = (MA (\/) MB) . i

for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) (\/) (MSUnion B)

let M be ManySortedSet of I; :: 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 I ;

reconsider MA = MSUnion A as ManySortedSubset of M ;

reconsider MA = MA as ManySortedSet of I ;

reconsider MB = MSUnion B as ManySortedSubset of M ;

reconsider MB = MB as ManySortedSet of I ;

for i being object st i in I holds

MAB . i = (MA (\/) MB) . i

proof

hence
MSUnion (A \/ B) = (MSUnion A) (\/) (MSUnion B)
; :: thesis: verum
let i be object ; :: 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 Def2;

A3: (MA (\/) MB) . i = (MA . i) \/ (MB . i) by A1, PBOOLE:def 4;

A4: for v being object st v in (MA (\/) MB) . i holds

v in MAB . i

for v being object st v in MAB . i holds

v in (MA (\/) MB) . i

end;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 Def2;

A3: (MA (\/) MB) . i = (MA . i) \/ (MB . i) by A1, PBOOLE:def 4;

A4: for v being object st v in (MA (\/) MB) . i holds

v in MAB . i

proof

A14:
( MA . i = union { (f . i) where f is Element of Bool M : f in A } & MB . i = union { (f . i) where f is Element of Bool M : f in B } )
by A1, Def2;
let v be object ; :: thesis: ( v in (MA (\/) MB) . i implies v in MAB . i )

assume v in (MA (\/) MB) . i ; :: thesis: v in MAB . i

then A5: ( v in MA . i or v in MB . i ) by A3, XBOOLE_0:def 3;

end;assume v in (MA (\/) MB) . i ; :: thesis: v in MAB . i

then A5: ( 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, A5, Def2;

end;

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

A6: v in g and

A7: 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

A8: g = h . i and

A9: h in A by A7;

h in A \/ B by A9, XBOOLE_0:def 3;

then g in { (f . i) where f is Element of Bool M : f in A \/ B } by A8;

hence v in MAB . i by A2, A6, TARSKI:def 4; :: thesis: verum

end;A6: v in g and

A7: 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

A8: g = h . i and

A9: h in A by A7;

h in A \/ B by A9, XBOOLE_0:def 3;

then g in { (f . i) where f is Element of Bool M : f in A \/ B } by A8;

hence v in MAB . i by A2, A6, TARSKI:def 4; :: thesis: verum

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

A10: v in g and

A11: 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

A12: g = h . i and

A13: h in B by A11;

h in A \/ B by A13, XBOOLE_0:def 3;

then g in { (f . i) where f is Element of Bool M : f in A \/ B } by A12;

hence v in MAB . i by A2, A10, TARSKI:def 4; :: thesis: verum

end;A10: v in g and

A11: 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

A12: g = h . i and

A13: h in B by A11;

h in A \/ B by A13, XBOOLE_0:def 3;

then g in { (f . i) where f is Element of Bool M : f in A \/ B } by A12;

hence v in MAB . i by A2, A10, TARSKI:def 4; :: thesis: verum

for v being object st v in MAB . i holds

v in (MA (\/) MB) . i

proof

hence
MAB . i = (MA (\/) MB) . i
by A4, TARSKI:2; :: thesis: verum
let v be object ; :: 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

A15: v in h and

A16: 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

A17: h = g . i and

A18: g in A \/ B by A16;

( g in A or g in B ) by A18, 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 A17;

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 A15, TARSKI:def 4;

hence v in (MA (\/) MB) . i by A3, A14, XBOOLE_0:def 3; :: thesis: verum

end;assume v in MAB . i ; :: thesis: v in (MA (\/) MB) . i

then consider h being set such that

A15: v in h and

A16: 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

A17: h = g . i and

A18: g in A \/ B by A16;

( g in A or g in B ) by A18, 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 A17;

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 A15, TARSKI:def 4;

hence v in (MA (\/) MB) . i by A3, A14, XBOOLE_0:def 3; :: thesis: verum