hereby :: thesis: ( not I <> {} implies ex b₁ being ManySortedSet of st b₁ = {} )

assume I <> {} ; :: thesis: ex f being ManySortedSet of st
for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & f . i = the Sorts of U0 . s )
then reconsider I' = I as non empty set ;
reconsider A' = A as MSAlgebra-Family of I',S ;
deffunc H₁( Element of I') -> set = the Sorts of (A' . $1) . s;
consider f being Function such that
A1: ( dom f = I' & ( for i being Element of I' holds f . i = H₁(i) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of by A1, PARTFUN1:def 4, RELAT_1:def 18;
take f = f; :: thesis: for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & f . i = the Sorts of U0 . s )
let i be set ; :: thesis: ( i in I implies ex U0 being MSAlgebra of S st
( U0 = A . i & f . i = the Sorts of U0 . s ) )
assume i in I ; :: thesis: ex U0 being MSAlgebra of S st
( U0 = A . i & f . i = the Sorts of U0 . s )
then reconsider i' = i as Element of I' ;
reconsider U0 = A' . i' as MSAlgebra of S ;
take U0 = U0; :: thesis: ( U0 = A . i & f . i = the Sorts of U0 . s )
thus ( U0 = A . i & f . i = the Sorts of U0 . s ) by A1; :: thesis: verum

end;

assume A2: I = {} ; :: thesis: ex b₁ being ManySortedSet of st b₁ = {}
take [0] I ; :: thesis: [0] I = {}
thus [0] I = {} by A2; :: thesis: verum