A3:
dom ( the Sorts of U1 * (the_arity_of o)) = (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o))))
now let e be
set ;
( e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) implies ( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e) )A8:
product ( the Sorts of U2 * (the_arity_of o)) <> {}
by A2, PRALG_2:10;
assume
e in (F * (the_arity_of o)) " (SubFuncs (rng (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))
by FUNCT_6:28;
then A9:
e in dom (the_arity_of o)
by FUNCT_1:21;
then reconsider f =
e as
Element of
NAT ;
(the_arity_of o) . f in the
carrier of
S
by A9, FINSEQ_2:13;
then
(the_arity_of o) . e in dom the
Sorts of
U2
by PARTFUN1:def 4;
then A10:
e in dom ( the Sorts of U2 * (the_arity_of o))
by A9, FUNCT_1:21;
A11:
( the Sorts of U2 * (the_arity_of o)) . e = the
Sorts of
U2 . ((the_arity_of o) . e)
by A9, FUNCT_1:23;
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 A9, FINSEQ_2:13, PBOOLE:def 18;
thus ( the Sorts of U1 * (the_arity_of o)) . e =
the
Sorts of
U1 . ((the_arity_of o) . e)
by A9, FUNCT_1:23
.=
dom Foe
by A12, FUNCT_2:def 1
.=
proj1 Foe
.=
proj1 ((F * (the_arity_of o)) . e)
by A9, FUNCT_1:23
;
verum end;
then A13:
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 A14:
x in product ( the Sorts of U1 * (the_arity_of o))
by PRALG_2:10;
then consider f being Function such that
A15:
x = f
and
dom f = dom (doms (F * (the_arity_of o)))
and
A16:
for e being set st e in dom (doms (F * (the_arity_of o))) holds
f . e in (doms (F * (the_arity_of o))) . e
by A13, CARD_3:def 5;
A17:
dom ((F * (the_arity_of o)) .. f) = dom (F * (the_arity_of o))
by PRALG_1:def 17;
A18:
rng (the_arity_of o) c= the carrier of S
by FINSEQ_1:def 4;
then A19:
rng (the_arity_of o) c= dom the Sorts of U2
by PARTFUN1:def 4;
rng (the_arity_of o) c= dom F
by A18, PARTFUN1:def 4;
then A20: dom (F * (the_arity_of o)) =
dom (the_arity_of o)
by RELAT_1:46
.=
dom ( the Sorts of U2 * (the_arity_of o))
by A19, RELAT_1:46
;
A21:
now let e be
set ;
( 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 )A22:
product ( the Sorts of U2 * (the_arity_of o)) <> {}
by A2, PRALG_2:10;
assume A23:
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 A24:
e in dom (the_arity_of o)
by FUNCT_1:21;
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:13, PBOOLE:def 18;
reconsider r =
e as
Element of
NAT by A24;
g = (F * (the_arity_of o)) . e
by A20, A23, FUNCT_1:22;
then A25:
((F * (the_arity_of o)) .. f) . e = g . (f . e)
by A20, A23, PRALG_1:def 17;
A26:
( the Sorts of U2 * (the_arity_of o)) . e = the
Sorts of
U2 . ((the_arity_of o) . e)
by A24, FUNCT_1:23;
(the_arity_of o) . r in the
carrier of
S
by A24, FINSEQ_2:13;
then
(the_arity_of o) . e in dom the
Sorts of
U1
by PARTFUN1:def 4;
then
e in dom ( the Sorts of U1 * (the_arity_of o))
by A24, FUNCT_1:21;
then
f . e in (doms (F * (the_arity_of o))) . e
by A13, A16;
then
f . e in the
Sorts of
U1 . ((the_arity_of o) . e)
by A13, A24, FUNCT_1:23;
then
g . (f . e) in the
Sorts of
U2 . ((the_arity_of o) . e)
by A27, FUNCT_2:7;
hence
((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . e
by A23, A25, FUNCT_1:22;
verum end;
(Frege (F * (the_arity_of o))) . x = (F * (the_arity_of o)) .. f
by A14, A13, A15, PRALG_2:def 8;
then
(Frege (F * (the_arity_of o))) . x in product ( the Sorts of U2 * (the_arity_of o))
by A17, A20, A21, CARD_3:18;
hence
(Frege (F * (the_arity_of o))) . x is Element of Args (o,U2)
by PRALG_2:10; verum