let f, g be ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S; :: thesis: ( ( for o being OperSymbol of S holds f . o = QuotRes R,o ) & ( for o being OperSymbol of S holds g . o = QuotRes R,o ) implies f = g )
assume that
A5: for o being OperSymbol of S holds f . o = QuotRes R,o and
A6: for o being OperSymbol of S holds g . o = QuotRes R,o ; :: thesis: f = g

now

let i be set ; :: 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 i1 = i as OperSymbol of S ;
( f . i1 = QuotRes R,i1 & g . i1 = QuotRes R,i1 ) by A5, A6;
hence f . i = g . i ; :: thesis: verum

end;

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