A3:
dom ( the Sorts of U1 * (the_arity_of o)) = dom (F * (the_arity_of o))

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 ;

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; :: thesis: verum

proof

assume e in dom (F * (the_arity_of o)) ; :: thesis: e in dom ( the Sorts of U1 * (the_arity_of o))

then e in dom (F * (the_arity_of o)) ;

then A6: 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 A6, FINSEQ_2:11;

then (the_arity_of o) . e in dom the Sorts of U1 by PARTFUN1:def 2;

hence e in dom ( the Sorts of U1 * (the_arity_of o)) by A6, FUNCT_1:11; :: thesis: verum

end;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: dom (F * (the_arity_of o)) c= dom ( the Sorts of U1 * (the_arity_of o))

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in dom (F * (the_arity_of o)) or e in dom ( the Sorts of U1 * (the_arity_of o)) )let e be object ; :: thesis: ( e in dom ( the Sorts of U1 * (the_arity_of o)) implies e in dom (F * (the_arity_of o)) )

assume A4: e in dom ( the Sorts of U1 * (the_arity_of o)) ; :: thesis: e in dom (F * (the_arity_of o))

then (the_arity_of o) . e in dom the Sorts of U1 by FUNCT_1:11;

then (the_arity_of o) . e in the carrier of S by PARTFUN1:def 2;

then A5: (the_arity_of o) . e in dom F by PARTFUN1:def 2;

e in dom (the_arity_of o) by A4, FUNCT_1:11;

then e in dom (F * (the_arity_of o)) by A5, FUNCT_1:11;

hence e in dom (F * (the_arity_of o)) ; :: thesis: verum

end;assume A4: e in dom ( the Sorts of U1 * (the_arity_of o)) ; :: thesis: e in dom (F * (the_arity_of o))

then (the_arity_of o) . e in dom the Sorts of U1 by FUNCT_1:11;

then (the_arity_of o) . e in the carrier of S by PARTFUN1:def 2;

then A5: (the_arity_of o) . e in dom F by PARTFUN1:def 2;

e in dom (the_arity_of o) by A4, FUNCT_1:11;

then e in dom (F * (the_arity_of o)) by A5, FUNCT_1:11;

hence e in dom (F * (the_arity_of o)) ; :: thesis: verum

assume e in dom (F * (the_arity_of o)) ; :: thesis: e in dom ( the Sorts of U1 * (the_arity_of o))

then e in dom (F * (the_arity_of o)) ;

then A6: 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 A6, FINSEQ_2:11;

then (the_arity_of o) . e in dom the Sorts of U1 by PARTFUN1:def 2;

hence e in dom ( the Sorts of U1 * (the_arity_of o)) by A6, FUNCT_1:11; :: thesis: verum

now :: thesis: 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)

then A12:
the Sorts of U1 * (the_arity_of o) = doms (F * (the_arity_of o))
by A3, FUNCT_6:def 2;( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e)

let e be object ; :: thesis: ( 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)) ; :: thesis: ( 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;

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 ; :: thesis: verum

end;A7: product ( the Sorts of U2 * (the_arity_of o)) <> {} by A2, PRALG_2:3;

assume e in dom (F * (the_arity_of o)) ; :: thesis: ( 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;

A11: now :: thesis: not the Sorts of U2 . ((the_arity_of o) . e) = {}

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;assume
the Sorts of U2 . ((the_arity_of o) . e) = {}
; :: thesis: contradiction

then {} in rng ( the Sorts of U2 * (the_arity_of o)) by A9, A10, FUNCT_1:def 3;

hence contradiction by A7, CARD_3:26; :: thesis: verum

end;then {} in rng ( the Sorts of U2 * (the_arity_of o)) by A9, A10, FUNCT_1:def 3;

hence contradiction by A7, CARD_3:26; :: thesis: verum

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 ; :: thesis: verum

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 :: thesis: 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)) . e

(Frege (F * (the_arity_of o))) . x = (F * (the_arity_of o)) .. f
by A13, A12, A14, PRALG_2:def 2;((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . e

let e be object ; :: thesis: ( 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)) ; :: thesis: ((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . e

then 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;

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; :: thesis: verum

end;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)) ; :: thesis: ((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . e

then 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;

A26: now :: thesis: not the Sorts of U2 . ((the_arity_of o) . e) = {}

(the_arity_of o) . r in the carrier of S
by A23, FINSEQ_2:11;assume
the Sorts of U2 . ((the_arity_of o) . e) = {}
; :: thesis: contradiction

then {} in rng ( the Sorts of U2 * (the_arity_of o)) by A22, A25, FUNCT_1:def 3;

hence contradiction by A21, CARD_3:26; :: thesis: verum

end;then {} in rng ( the Sorts of U2 * (the_arity_of o)) by A22, A25, FUNCT_1:def 3;

hence contradiction by A21, CARD_3:26; :: thesis: verum

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; :: thesis: verum

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; :: thesis: verum