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

assume I <> {} ; :: thesis: ex X being ManySortedFunction of st
for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & X . i = the Charact of U0 )
then reconsider I' = I as non empty set ;
reconsider A' = A as MSAlgebra-Family of I',S ;
deffunc H₁( Element of I') -> ManySortedFunction of the Arity of S * (the Sorts of (A' . $1) # ),the ResultSort of S * the Sorts of (A' . $1) = the Charact of (A' . $1);
consider X being ManySortedSet of such that
A1: for i being Element of I' holds X . i = H₁(i) from PBOOLE:sch 5();
for x being set st x in dom X holds
X . x is Function

proof

let x be set ; :: thesis: ( x in dom X implies X . x is Function )
assume x in dom X ; :: thesis: X . x is Function
then reconsider i = x as Element of I' by PARTFUN1:def 4;
X . i = the Charact of (A' . i) by A1;
hence X . x is Function ; :: thesis: verum

end;

then reconsider X = X as ManySortedFunction of by FUNCOP_1:def 6;
take X = X; :: thesis: for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & X . i = the Charact of U0 )
let i be set ; :: thesis: ( i in I implies ex U0 being MSAlgebra of S st
( U0 = A . i & X . i = the Charact of U0 ) )
assume i in I ; :: thesis: ex U0 being MSAlgebra of S st
( U0 = A . i & X . i = the Charact of U0 )
then reconsider i' = i as Element of I' ;
reconsider U0 = A' . i' as MSAlgebra of S ;
take U0 = U0; :: thesis: ( U0 = A . i & X . i = the Charact of U0 )
thus ( U0 = A . i & X . i = the Charact of U0 ) by A1; :: thesis: verum

end;

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