let B1, B2 be ManySortedSubset of M; :: thesis: ( ( for i being set st i in I holds

B1 . i = union { (f . i) where f is Element of Bool M : f in A } ) & ( for i being set st i in I holds

B2 . i = union { (f . i) where f is Element of Bool M : f in A } ) implies B1 = B2 )

assume that

A9: for i being set st i in I holds

B1 . i = union { (f . i) where f is Element of Bool M : f in A } and

A10: for i being set st i in I holds

B2 . i = union { (ff . i) where ff is Element of Bool M : ff in A } ; :: thesis: B1 = B2

for i being object st i in I holds

B1 . i = B2 . i

B1 . i = union { (f . i) where f is Element of Bool M : f in A } ) & ( for i being set st i in I holds

B2 . i = union { (f . i) where f is Element of Bool M : f in A } ) implies B1 = B2 )

assume that

A9: for i being set st i in I holds

B1 . i = union { (f . i) where f is Element of Bool M : f in A } and

A10: for i being set st i in I holds

B2 . i = union { (ff . i) where ff is Element of Bool M : ff in A } ; :: thesis: B1 = B2

for i being object st i in I holds

B1 . i = B2 . i

proof

hence
B1 = B2
; :: thesis: verum
let i be object ; :: thesis: ( i in I implies B1 . i = B2 . i )

assume A11: i in I ; :: thesis: B1 . i = B2 . i

then B1 . i = union { (f . i) where f is Element of Bool M : f in A } by A9

.= B2 . i by A10, A11 ;

hence B1 . i = B2 . i ; :: thesis: verum

end;assume A11: i in I ; :: thesis: B1 . i = B2 . i

then B1 . i = union { (f . i) where f is Element of Bool M : f in A } by A9

.= B2 . i by A10, A11 ;

hence B1 . i = B2 . i ; :: thesis: verum