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
proof
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;
hence B1 = B2 ; :: thesis: verum