A3: dom ( the Sorts of U1 * (the_arity_of o)) = dom (F * (the_arity_of o))
proof
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 ; :: 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;
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)) )
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;
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)
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;
A11: now :: thesis: not the Sorts of U2 . ((the_arity_of o) . e) = {}
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;
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 ; :: thesis: 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 :: 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
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;
A26: now :: thesis: not the Sorts of U2 . ((the_arity_of o) . e) = {}
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;
(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; :: thesis: 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; :: thesis: verum