let f, g be ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S; :: thesis: ( ( for o being OperSymbol of S holds f . o = OSQuotArgs (R,o) ) & ( for o being OperSymbol of S holds g . o = OSQuotArgs (R,o) ) implies f = g )
assume that
A7: for o being OperSymbol of S holds f . o = OSQuotArgs (R,o) and
A8: for o being OperSymbol of S holds g . o = OSQuotArgs (R,o) ; :: thesis: f = g
now :: thesis: for i being object st i in the carrier' of S holds
f . i = g . i
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 i1 = i as OperSymbol of S ;
f . i1 = OSQuotArgs (R,i1) by A7;
hence f . i = g . i by A8; :: thesis: verum
end;
hence f = g by PBOOLE:3; :: thesis: verum