set ar = the_arity_of o;
set da = dom (the_arity_of o);
defpred S₁[ set , set ] means for n being Nat st n = $1 holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & $2 = OSClass R,y );
A1: for k being set st k in dom (the_arity_of o) holds
ex u being set st S₁[k,u]

proof

let k be set ; :: thesis: ( k in dom (the_arity_of o) implies ex u being set st S₁[k,u] )
assume A2: k in dom (the_arity_of o) ; :: thesis: ex u being set st S₁[k,u]
then reconsider n = k as Nat ;
reconsider y = x . n as Element of the Sorts of A . ((the_arity_of o) /. n) by A2, MSUALG_6:2;
take OSClass R,y ; :: thesis: S₁[k, OSClass R,y]
thus S₁[k, OSClass R,y] ; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = dom (the_arity_of o) & ( for x being set st x in dom (the_arity_of o) holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A1);
A4: dom ((OSClass R) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 4;
for y being set st y in dom ((OSClass R) * (the_arity_of o)) holds
f . y in ((OSClass R) * (the_arity_of o)) . y

proof

let y be set ; :: thesis: ( y in dom ((OSClass R) * (the_arity_of o)) implies f . y in ((OSClass R) * (the_arity_of o)) . y )
assume A5: y in dom ((OSClass R) * (the_arity_of o)) ; :: thesis: f . y in ((OSClass R) * (the_arity_of o)) . y
then A6: ((OSClass R) * (the_arity_of o)) . y = (OSClass R) . ((the_arity_of o) . y) by FUNCT_1:22;
(the_arity_of o) . y in rng (the_arity_of o) by A4, A5, FUNCT_1:def 5;
then reconsider s = (the_arity_of o) . y as Element of S ;
reconsider n = y as Nat by A5;
consider z being Element of the Sorts of A . ((the_arity_of o) /. n) such that
A7: ( z = x . n & f . n = OSClass R,z ) by A3, A4, A5;
(the_arity_of o) /. n = (the_arity_of o) . n by A4, A5, PARTFUN1:def 8;
then f . y in OSClass R,s by A7;
hence f . y in ((OSClass R) * (the_arity_of o)) . y by A6, Def13; :: thesis: verum

end;

then reconsider f = f as Element of product ((OSClass R) * (the_arity_of o)) by A3, A4, CARD_3:18;
take f ; :: thesis: for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & f . n = OSClass R,y )
let n be Nat; :: thesis: ( n in dom (the_arity_of o) implies ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & f . n = OSClass R,y ) )
assume n in dom (the_arity_of o) ; :: thesis: ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & f . n = OSClass R,y )
hence ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & f . n = OSClass R,y ) by A3; :: thesis: verum