let f, g be ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S; :: thesis:

hereby :: thesis:

assume I <> {} ; :: thesis:
assume that
A88: for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) and
A89: for o being OperSymbol of S holds g . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ; :: thesis:
for i being object st i in the carrier' of S holds
f . i = g . i

proof

let i be object ; :: thesis:
assume i in the carrier' of S ; :: thesis:
then reconsider o = i as Element of the carrier' of S ;
f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A88;
hence f . i = g . i by A89; :: thesis:

end;

hence f = g ; :: thesis:

end;

assume A90: I = {} ; :: thesis:

A91: now :: thesis:

let o be object ; :: thesis:
assume A92: o in the carrier' of S ; :: thesis:
then reconsider s = the ResultSort of S . o as SortSymbol of S by FUNCT_2:5;
o in dom the ResultSort of S by A92, FUNCT_2:def 1;
then A93: ((SORTS A) * the ResultSort of S) . o = (SORTS A) . s by FUNCT_1:13
.= product (Carrier (A,s)) by Def10
.= {{}} by A90, CARD_3:10 ;
( f . o is Function of ((((SORTS A) #) * the Arity of S) . o),(((SORTS A) * the ResultSort of S) . o) & g . o is Function of ((((SORTS A) #) * the Arity of S) . o),(((SORTS A) * the ResultSort of S) . o) ) by A92, PBOOLE:def 15;
hence f . o = g . o by A93, FUNCT_2:51; :: thesis:

end;

thus f = g by A91; :: thesis: