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

assume I <> {} ; :: thesis: ex f being ManySortedSet of I st
for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Sorts of U0 . s )
then reconsider I9 = I as non empty set ;
reconsider A9 = A as MSAlgebra-Family of I9,S ;
deffunc H₁( Element of I9) -> set = the Sorts of (A9 . $1) . s;
consider f being Function such that
A1: ( dom f = I9 & ( for i being Element of I9 holds f . i = H₁(i) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;
take f = f; :: thesis: for i being set st i in I holds
ex U0 being MSAlgebra over 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 over S st
( U0 = A . i & f . i = the Sorts of U0 . s ) )
assume i in I ; :: thesis: ex U0 being MSAlgebra over S st
( U0 = A . i & f . i = the Sorts of U0 . s )
then reconsider i9 = i as Element of I9 ;
reconsider U0 = A9 . i9 as MSAlgebra over 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 I st b₁ = {}
take EmptyMS I ; :: thesis: EmptyMS I = {}
thus EmptyMS I = {} by A2; :: thesis: verum