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
$2 = Class (R . ((the_arity_of o) /. n)),(x . n);
A1: for y being set st y in dom (the_arity_of o) holds
ex u being set st S₁[y,u]

proof

let y be set ; :: thesis: ( y in dom (the_arity_of o) implies ex u being set st S₁[y,u] )
assume y in dom (the_arity_of o) ; :: thesis: ex u being set st S₁[y,u]
then reconsider n = y as Nat by ORDINAL1:def 13;
take Class (R . ((the_arity_of o) /. n)),(x . n) ; :: thesis: S₁[y, Class (R . ((the_arity_of o) /. n)),(x . n)]
thus S₁[y, Class (R . ((the_arity_of o) /. n)),(x . n)] ; :: thesis: verum

end;

consider f being Function such that
A2: ( 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);
A3: dom ((Class R) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 4;
for y being set st y in dom ((Class R) * (the_arity_of o)) holds
f . y in ((Class R) * (the_arity_of o)) . y

proof

let y be set ; :: thesis: ( y in dom ((Class R) * (the_arity_of o)) implies f . y in ((Class R) * (the_arity_of o)) . y )
assume A4: y in dom ((Class R) * (the_arity_of o)) ; :: thesis: f . y in ((Class R) * (the_arity_of o)) . y
then A5: ((Class R) * (the_arity_of o)) . y = (Class R) . ((the_arity_of o) . y) by FUNCT_1:22;
(the_arity_of o) . y in rng (the_arity_of o) by A3, A4, FUNCT_1:def 5;
then reconsider s = (the_arity_of o) . y as Element of S ;
reconsider n = y as Nat by A3, A4, ORDINAL1:def 13;
A6: f . n = Class (R . ((the_arity_of o) /. n)),(x . n) by A2, A3, A4;
A7: (the_arity_of o) /. n = (the_arity_of o) . n by A3, A4, PARTFUN1:def 8;
A8: y in dom (the Sorts of A * (the_arity_of o)) by A3, A4, PARTFUN1:def 4;
then (the Sorts of A * (the_arity_of o)) . y = the Sorts of A . ((the_arity_of o) . y) by FUNCT_1:22;
then x . y in the Sorts of A . s by A8, MSUALG_3:6;
then f . y in Class (R . s) by A6, A7, EQREL_1:def 5;
hence f . y in ((Class R) * (the_arity_of o)) . y by A5, Def8; :: thesis: verum

end;

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