reconsider f = EmptyMS I as ManySortedFunction of I ;

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

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

proof

let x be object ; :: 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 I9 by PARTFUN1:def 2;
X . i = the Charact of (A9 . i) by A1;
hence X . x is Function ; :: thesis: verum

end;

then reconsider X = X as ManySortedFunction of I by FUNCOP_1:def 6;
take X = X; :: thesis: for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & X . i = the Charact of U0 )
let i be set ; :: thesis: ( i in I implies ex U0 being MSAlgebra over S st
( U0 = A . i & X . i = the Charact of U0 ) )
assume i in I ; :: thesis: ex U0 being MSAlgebra over S st
( U0 = A . i & X . i = the Charact of U0 )
then reconsider i9 = i as Element of I9 ;
reconsider U0 = A9 . i9 as MSAlgebra over 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 I st b₁ = {}
take f ; :: thesis: f = {}
thus f = {} by A2; :: thesis: verum