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

proof

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

proof

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;

hence MA . i c= MB . i ; :: thesis: verum

end;

hence MSUnion A c= MSUnion B ; :: thesis: verum