let f, g be ManySortedFunction 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 Charact of U0 ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & g . i = the Charact of U0 ) ) 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 Charact of U0 ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & g . i = the Charact of U0 ) ) 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 Charact of U0 ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & g . i = the Charact of U0 ) ) ) ; :: 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 Charact of U0 ) & ex U0 being MSAlgebra over S st
( U0 = A . i & g . i = the Charact of U0 ) ) 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