set ao = the_arity_of o;
let F, G be Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o); :: thesis: ( ( for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
F . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ) & ( for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
G . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ) implies F = G )
assume that
A14: for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
F . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a and
A15: for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
G . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ; :: thesis: F = G
A16: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then dom (((OSClass R) #) * the Arity of S) = dom the Arity of S by PARTFUN1:def 2;
then A17: (((OSClass R) #) * the Arity of S) . o = ((OSClass R) #) . ( the Arity of S . o) by A16, FUNCT_1:12
.= ((OSClass R) #) . (the_arity_of o) by MSUALG_1:def 1 ;

A18: now :: thesis: for x being object st x in ((OSClass R) #) . (the_arity_of o) holds
F . x = G . x

let x be object ; :: thesis: ( x in ((OSClass R) #) . (the_arity_of o) implies F . x = G . x )
assume A19: x in ((OSClass R) #) . (the_arity_of o) ; :: thesis: F . x = G . x
then consider a being Element of Args (o,A) such that
A20: x = R #_os a by A17, Th14;
F . x = ((OSQuotRes (R,o)) * (Den (o,A))) . a by A14, A17, A19, A20;
hence F . x = G . x by A15, A17, A19, A20; :: thesis: verum

end;

( dom F = ((OSClass R) #) . (the_arity_of o) & dom G = ((OSClass R) #) . (the_arity_of o) ) by A17, FUNCT_2:def 1;
hence F = G by A18, FUNCT_1:2; :: thesis: verum