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
A82: for o being OperSymbol of S holds f . o = IFEQ (the_arity_of o),{} ,(commute (A ?. o)),(Commute (Frege (A ?. o))) and
A83: 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 set st i in the carrier' of S holds
f . i = g . i

let i be set ; :: 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))) & g . o = IFEQ (the_arity_of o),{} ,(commute (A ?. o)),(Commute (Frege (A ?. o))) ) by A82, A83;
hence f . i = g . i ; :: thesis:

end;

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

end;

assume A84: I = {} ; :: thesis:
A85: dom f = the carrier' of S by PARTFUN1:def 4;
A86: dom g = the carrier' of S by PARTFUN1:def 4;

let o be set ; :: thesis:
assume A87: o in the carrier' of S ; :: thesis:
then reconsider s = the ResultSort of S . o as SortSymbol of S by FUNCT_2:7;
o in dom the ResultSort of S by A87, FUNCT_2:def 1;
then A88: ((SORTS A) * the ResultSort of S) . o = (SORTS A) . s by FUNCT_1:23
.= product (Carrier A,s) by Def17
.= {{} } by A84, Def16, CARD_3:19 ;
A89: f . o is Function of ((((SORTS A) # ) * the Arity of S) . o),(((SORTS A) * the ResultSort of S) . o) by A87, PBOOLE:def 18;
g . o is Function of ((((SORTS A) # ) * the Arity of S) . o),(((SORTS A) * the ResultSort of S) . o) by A87, PBOOLE:def 18;
hence f . o = g . o by A88, A89, FUNCT_2:66; :: thesis:

end;

hence f = g by A85, A86, FUNCT_1:9; :: thesis: