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

for A, B being SubsetFamily of M st A c= B holds

MSUnion A c= MSUnion B

let M be ManySortedSet of I; :: thesis: for A, B being SubsetFamily of M st A c= B holds

MSUnion A c= MSUnion B

let A, B be SubsetFamily of M; :: thesis: ( A c= B implies MSUnion A c= MSUnion B )

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 ;

assume A1: A c= B ; :: thesis: MSUnion A c= MSUnion B

for i being object st i in I holds

MA . i c= MB . i

for A, B being SubsetFamily of M st A c= B holds

MSUnion A c= MSUnion B

let M be ManySortedSet of I; :: thesis: for A, B being SubsetFamily of M st A c= B holds

MSUnion A c= MSUnion B

let A, B be SubsetFamily of M; :: thesis: ( A c= B implies MSUnion A c= MSUnion B )

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 ;

assume A1: A c= B ; :: thesis: MSUnion A c= MSUnion B

for i being object st i in I holds

MA . i c= MB . i

proof

hence
MSUnion A c= MSUnion B
; :: thesis: verum
let i be object ; :: thesis: ( i in I implies MA . i c= MB . i )

assume A2: i in I ; :: thesis: MA . i c= MB . i

for v being object st v in MA . i holds

v in MB . i

end;assume A2: i in I ; :: thesis: MA . i c= MB . i

for v being object st v in MA . i holds

v in MB . i

proof

hence
MA . i c= MB . i
; :: thesis: verum
A3:
MA . i = union { (f . i) where f is Element of Bool M : f in A }
by A2, Def2;

let v be object ; :: thesis: ( v in MA . i implies v in MB . i )

assume v in MA . i ; :: thesis: v in MB . i

then consider h being set such that

A4: v in h and

A5: h in { (f . i) where f is Element of Bool M : f in A } by A3, TARSKI:def 4;

ex g being Element of Bool M st

( h = g . i & g in A ) by A5;

then h in { (k . i) where k is Element of Bool M : k in B } by A1;

then v in union { (k . i) where k is Element of Bool M : k in B } by A4, TARSKI:def 4;

hence v in MB . i by A2, Def2; :: thesis: verum

end;let v be object ; :: thesis: ( v in MA . i implies v in MB . i )

assume v in MA . i ; :: thesis: v in MB . i

then consider h being set such that

A4: v in h and

A5: h in { (f . i) where f is Element of Bool M : f in A } by A3, TARSKI:def 4;

ex g being Element of Bool M st

( h = g . i & g in A ) by A5;

then h in { (k . i) where k is Element of Bool M : k in B } by A1;

then v in union { (k . i) where k is Element of Bool M : k in B } by A4, TARSKI:def 4;

hence v in MB . i by A2, Def2; :: thesis: verum