let f, g be ManySortedSet of ; :: thesis: ( ( I <> {} & ( 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 ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & g . i = the Sorts of U0 . s ) ) implies f = g ) & ( not I <> {} & f = {} & g = {} implies f = g ) )

hereby :: thesis: ( not I <> {} & f = {} & g = {} implies f = g )

assume I <> {} ; :: 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 ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & g . i = the Sorts of U0 . s ) ) implies f = g )
assume that
A3: 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 ) and
A4: for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & g . i = the Sorts of U0 . s ) ; :: thesis: f = g
for x being set st x in I holds
f . x = g . x

proof

let x be set ; :: thesis: ( x in I implies f . x = g . x )
assume A5: x in I ; :: thesis: f . x = g . x
then reconsider i = x as Element of I ;
( ex U0 being MSAlgebra of S st
( U0 = A . i & f . i = the Sorts of U0 . s ) & ex U0 being MSAlgebra of S st
( U0 = A . i & g . i = the Sorts of U0 . s ) ) by A3, A4, A5;
hence f . x = g . x ; :: thesis: verum

end;

hence f = g by PBOOLE:3; :: thesis: verum

end;

thus ( not I <> {} & f = {} & g = {} implies f = g ) ; :: thesis: verum