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

proof

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

end;

hence f = g ; :: thesis: verum

end;

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