defpred S1[ 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 S1[y,u]
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
S1[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 ;
( 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))
;
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;
verum
end;
then reconsider f = f as Element of product ((Class R) * (the_arity_of o)) by A2, A3, CARD_3:9;
take
f
; 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; ( 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)
; 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; verum