A3:
dom ( the Sorts of U1 * (the_arity_of o)) = dom (F * (the_arity_of o))
now for e being object st e in dom (F * (the_arity_of o)) holds
( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e)let e be
object ;
( e in dom (F * (the_arity_of o)) implies ( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e) )A7:
product ( the Sorts of U2 * (the_arity_of o)) <> {}
by A2, PRALG_2:3;
assume
e in dom (F * (the_arity_of o))
;
( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e)then
e in dom (F * (the_arity_of o))
;
then A8:
e in dom (the_arity_of o)
by FUNCT_1:11;
then reconsider f =
e as
Element of
NAT ;
(the_arity_of o) . f in the
carrier of
S
by A8, FINSEQ_2:11;
then
(the_arity_of o) . e in dom the
Sorts of
U2
by PARTFUN1:def 2;
then A9:
e in dom ( the Sorts of U2 * (the_arity_of o))
by A8, FUNCT_1:11;
A10:
( the Sorts of U2 * (the_arity_of o)) . e = the
Sorts of
U2 . ((the_arity_of o) . e)
by A8, FUNCT_1:13;
reconsider Foe =
F . ((the_arity_of o) . e) as
Function of
( the Sorts of U1 . ((the_arity_of o) . e)),
( the Sorts of U2 . ((the_arity_of o) . e)) by A8, FINSEQ_2:11, PBOOLE:def 15;
thus ( the Sorts of U1 * (the_arity_of o)) . e =
the
Sorts of
U1 . ((the_arity_of o) . e)
by A8, FUNCT_1:13
.=
dom Foe
by A11, FUNCT_2:def 1
.=
proj1 ((F * (the_arity_of o)) . e)
by A8, FUNCT_1:13
;
verum end;
then A12:
the Sorts of U1 * (the_arity_of o) = doms (F * (the_arity_of o))
by A3, FUNCT_6:def 2;
x in Args (o,U1)
by A1;
then A13:
x in product ( the Sorts of U1 * (the_arity_of o))
by PRALG_2:3;
then consider f being Function such that
A14:
x = f
and
a14:
dom f = dom (doms (F * (the_arity_of o)))
and
A15:
for e being object st e in dom (doms (F * (the_arity_of o))) holds
f . e in (doms (F * (the_arity_of o))) . e
by A12, CARD_3:def 5;
AA:
dom (doms (F * (the_arity_of o))) = dom (F * (the_arity_of o))
by FUNCT_6:def 2;
A16: dom ((F * (the_arity_of o)) .. f) =
(dom (F * (the_arity_of o))) /\ (dom f)
by PRALG_1:def 19
.=
dom (F * (the_arity_of o))
by a14, AA
;
A17:
rng (the_arity_of o) c= the carrier of S
by FINSEQ_1:def 4;
then A18:
rng (the_arity_of o) c= dom the Sorts of U2
by PARTFUN1:def 2;
SS:
rng (the_arity_of o) c= dom F
by A17, PARTFUN1:def 2;
then A19: dom (F * (the_arity_of o)) =
dom (the_arity_of o)
by RELAT_1:27
.=
dom ( the Sorts of U2 * (the_arity_of o))
by A18, RELAT_1:27
;
A20:
now for e being object st e in dom ( the Sorts of U2 * (the_arity_of o)) holds
((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . elet e be
object ;
( e in dom ( the Sorts of U2 * (the_arity_of o)) implies ((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . e )A21:
product ( the Sorts of U2 * (the_arity_of o)) <> {}
by A2, PRALG_2:3;
assume A22:
e in dom ( the Sorts of U2 * (the_arity_of o))
;
((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . ethen A23:
e in dom (the_arity_of o)
by FUNCT_1:11;
then reconsider g =
F . ((the_arity_of o) . e) as
Function of
( the Sorts of U1 . ((the_arity_of o) . e)),
( the Sorts of U2 . ((the_arity_of o) . e)) by FINSEQ_2:11, PBOOLE:def 15;
dom f = dom (the_arity_of o)
by A14, A1, Th6;
then AC:
e in dom f
by A23;
then
e in dom (the_arity_of o)
by A1, A14, Th6;
then
e in dom (F * (the_arity_of o))
by SS, RELAT_1:27;
then
e in (dom (F * (the_arity_of o))) /\ (dom f)
by AC, XBOOLE_0:def 4;
then AB:
e in dom ((F * (the_arity_of o)) .. f)
by PRALG_1:def 19;
reconsider r =
e as
Element of
NAT by A23;
g = (F * (the_arity_of o)) . e
by A19, A22, FUNCT_1:12;
then A24:
((F * (the_arity_of o)) .. f) . e = g . (f . e)
by PRALG_1:def 19, AB;
A25:
( the Sorts of U2 * (the_arity_of o)) . e = the
Sorts of
U2 . ((the_arity_of o) . e)
by A23, FUNCT_1:13;
(the_arity_of o) . r in the
carrier of
S
by A23, FINSEQ_2:11;
then
(the_arity_of o) . e in dom the
Sorts of
U1
by PARTFUN1:def 2;
then
e in dom ( the Sorts of U1 * (the_arity_of o))
by A23, FUNCT_1:11;
then
f . e in (doms (F * (the_arity_of o))) . e
by A12, A15;
then
f . e in the
Sorts of
U1 . ((the_arity_of o) . e)
by A12, A23, FUNCT_1:13;
then
g . (f . e) in the
Sorts of
U2 . ((the_arity_of o) . e)
by A26, FUNCT_2:5;
hence
((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . e
by A22, A24, FUNCT_1:12;
verum end;
(Frege (F * (the_arity_of o))) . x = (F * (the_arity_of o)) .. f
by A13, A12, A14, PRALG_2:def 2;
then
(Frege (F * (the_arity_of o))) . x in product ( the Sorts of U2 * (the_arity_of o))
by A16, A19, A20, CARD_3:9;
hence
(Frege (F * (the_arity_of o))) . x is Element of Args (o,U2)
by PRALG_2:3; verum