defpred S₁[ object , object ] means for n being Nat st n = $1 holds
$2 = Class ((R . ((the_arity_of o) /. n)),(x . n));
set ar = the_arity_of o;
set da = dom (the_arity_of o);
A1: for y being object st y in dom (the_arity_of o) holds
ex u being object st S₁[y,u]

proof

let y be object ; :: thesis: ( y in dom (the_arity_of o) implies ex u being object st S₁[y,u] )
assume y in dom (the_arity_of o) ; :: thesis: ex u being object st S₁[y,u]
then reconsider n = y as Nat by ORDINAL1:def 12;
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 object 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 2;
for y being object 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 object ; :: 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 reconsider n = y as Nat by ORDINAL1:def 12;
(the_arity_of o) . y in rng (the_arity_of o) by A3, A4, FUNCT_1:def 3;
then reconsider s = (the_arity_of o) . y as Element of S ;
A5: y in dom ( the Sorts of A * (the_arity_of o)) by A3, A4, PARTFUN1:def 2;
then ( the Sorts of A * (the_arity_of o)) . y = the Sorts of A . ((the_arity_of o) . y) by FUNCT_1:12;
then A6: x . y in the Sorts of A . s by A5, MSUALG_3:6;
( f . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) & (the_arity_of o) /. n = (the_arity_of o) . n ) by A2, A3, A4, PARTFUN1:def 6;
then A7: f . y in Class (R . s) by A6, EQREL_1:def 3;
((Class R) * (the_arity_of o)) . y = (Class R) . ((the_arity_of o) . y) by A4, FUNCT_1:12;
hence f . y in ((Class R) * (the_arity_of o)) . y by A7, Def6; :: thesis: verum

end;

then reconsider f = f as Element of product ((Class R) * (the_arity_of o)) by A2, A3, CARD_3:9;
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