let A, B be ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S; :: thesis: ( ( for o being OperSymbol of S holds A . o = DenOp (o,X) ) & ( for o being OperSymbol of S holds B . o = DenOp (o,X) ) implies A = B )

assume that

A3: for o being OperSymbol of S holds A . o = DenOp (o,X) and

A4: for o being OperSymbol of S holds B . o = DenOp (o,X) ; :: thesis: A = B

for i being object st i in the carrier' of S holds

A . i = B . i

assume that

A3: for o being OperSymbol of S holds A . o = DenOp (o,X) and

A4: for o being OperSymbol of S holds B . o = DenOp (o,X) ; :: thesis: A = B

for i being object st i in the carrier' of S holds

A . i = B . i

proof

hence
A = B
; :: thesis: verum
let i be object ; :: thesis: ( i in the carrier' of S implies A . i = B . i )

assume i in the carrier' of S ; :: thesis: A . i = B . i

then reconsider s = i as OperSymbol of S ;

A . s = DenOp (s,X) by A3;

hence A . i = B . i by A4; :: thesis: verum

end;assume i in the carrier' of S ; :: thesis: A . i = B . i

then reconsider s = i as OperSymbol of S ;

A . s = DenOp (s,X) by A3;

hence A . i = B . i by A4; :: thesis: verum