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