let f, g be ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S; :: thesis: ( ( I <> {} & ( for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( for o being OperSymbol of S holds g . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) implies f = g ) & ( not I <> {} implies f = g ) )

hereby :: thesis: ( not I <> {} implies f = g )

assume I <> {} ; :: thesis: ( ( for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( for o being OperSymbol of S holds g . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) implies f = g )
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: f = g
for i being object st i in the carrier' of S holds
f . i = g . i

proof

let i be object ; :: thesis: ( i in the carrier' of S implies f . i = g . i )
assume i in the carrier' of S ; :: thesis: f . i = g . i
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: verum

end;

hence f = g ; :: thesis: verum

end;

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

A91: now :: thesis: for o being object st o in the carrier' of S holds
f . o = g . o

let o be object ; :: thesis: ( o in the carrier' of S implies f . o = g . o )
assume A92: o in the carrier' of S ; :: thesis: f . o = g . o
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: verum

end;

thus f = g by A91; :: thesis: verum