defpred S₁[ object , object ] 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) );
set ar = the_arity_of o;
set da = dom (the_arity_of o);
A1: for k being object st k in dom (the_arity_of o) holds
ex u being object st S₁[k,u]

proof

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

end;

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