A3: dom ( the Sorts of U1 * ()) = dom (F * ())
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: dom (F * ()) c= dom ( the Sorts of U1 * ())
let e be object ; :: thesis: ( e in dom ( the Sorts of U1 * ()) implies e in dom (F * ()) )
assume A4: e in dom ( the Sorts of U1 * ()) ; :: thesis: e in dom (F * ())
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 () by ;
then e in dom (F * ()) by ;
hence e in dom (F * ()) ; :: thesis: verum
end;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in dom (F * ()) or e in dom ( the Sorts of U1 * ()) )
assume e in dom (F * ()) ; :: thesis: e in dom ( the Sorts of U1 * ())
then e in dom (F * ()) ;
then A6: e in dom () by FUNCT_1:11;
then reconsider f = e as Element of NAT ;
(the_arity_of o) . f in the carrier of S by ;
then (the_arity_of o) . e in dom the Sorts of U1 by PARTFUN1:def 2;
hence e in dom ( the Sorts of U1 * ()) by ; :: thesis: verum
end;
now :: thesis: for e being object st e in dom (F * ()) holds
( the Sorts of U1 * ()) . e = proj1 ((F * ()) . e)
let e be object ; :: thesis: ( e in dom (F * ()) implies ( the Sorts of U1 * ()) . e = proj1 ((F * ()) . e) )
A7: product ( the Sorts of U2 * ()) <> {} by ;
assume e in dom (F * ()) ; :: thesis: ( the Sorts of U1 * ()) . e = proj1 ((F * ()) . e)
then e in dom (F * ()) ;
then A8: e in dom () by FUNCT_1:11;
then reconsider f = e as Element of NAT ;
(the_arity_of o) . f in the carrier of S by ;
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 * ()) by ;
A10: ( the Sorts of U2 * ()) . e = the Sorts of U2 . (() . e) by ;
A11: now :: thesis: not the Sorts of U2 . (() . e) = {}
assume the Sorts of U2 . (() . e) = {} ; :: thesis: contradiction
then {} in rng ( the Sorts of U2 * ()) by ;
hence contradiction by A7, CARD_3:26; :: thesis: verum
end;
reconsider Foe = F . (() . e) as Function of ( the Sorts of U1 . (() . e)),( the Sorts of U2 . (() . e)) by ;
thus ( the Sorts of U1 * ()) . e = the Sorts of U1 . (() . e) by
.= dom Foe by
.= proj1 ((F * ()) . e) by ; :: thesis: verum
end;
then A12: the Sorts of U1 * () = doms (F * ()) by ;
x in Args (o,U1) by A1;
then A13: x in product ( the Sorts of U1 * ()) by PRALG_2:3;
then consider f being Function such that
A14: x = f and
a14: dom f = dom (doms (F * ())) and
A15: for e being object st e in dom (doms (F * ())) holds
f . e in (doms (F * ())) . e by ;
AA: dom (doms (F * ())) = dom (F * ()) by FUNCT_6:def 2;
A16: dom ((F * ()) .. f) = (dom (F * ())) /\ (dom f) by PRALG_1:def 19
.= dom (F * ()) by ;
A17: rng () c= the carrier of S by FINSEQ_1:def 4;
then A18: rng () c= dom the Sorts of U2 by PARTFUN1:def 2;
SS: rng () c= dom F by ;
then A19: dom (F * ()) = dom () by RELAT_1:27
.= dom ( the Sorts of U2 * ()) by ;
A20: now :: thesis: for e being object st e in dom ( the Sorts of U2 * ()) holds
((F * ()) .. f) . e in ( the Sorts of U2 * ()) . e
let e be object ; :: thesis: ( e in dom ( the Sorts of U2 * ()) implies ((F * ()) .. f) . e in ( the Sorts of U2 * ()) . e )
A21: product ( the Sorts of U2 * ()) <> {} by ;
assume A22: e in dom ( the Sorts of U2 * ()) ; :: thesis: ((F * ()) .. f) . e in ( the Sorts of U2 * ()) . e
then A23: e in dom () by FUNCT_1:11;
then reconsider g = F . (() . e) as Function of ( the Sorts of U1 . (() . e)),( the Sorts of U2 . (() . e)) by ;
dom f = dom () by A14, A1, Th6;
then AC: e in dom f by A23;
then e in dom () by A1, A14, Th6;
then e in dom (F * ()) by ;
then e in (dom (F * ())) /\ (dom f) by ;
then AB: e in dom ((F * ()) .. f) by PRALG_1:def 19;
reconsider r = e as Element of NAT by A23;
g = (F * ()) . e by ;
then A24: ((F * ()) .. f) . e = g . (f . e) by ;
A25: ( the Sorts of U2 * ()) . e = the Sorts of U2 . (() . e) by ;
A26: now :: thesis: not the Sorts of U2 . (() . e) = {}
assume the Sorts of U2 . (() . e) = {} ; :: thesis: contradiction
then {} in rng ( the Sorts of U2 * ()) by ;
hence contradiction by A21, CARD_3:26; :: thesis: verum
end;
(the_arity_of o) . r in the carrier of S by ;
then (the_arity_of o) . e in dom the Sorts of U1 by PARTFUN1:def 2;
then e in dom ( the Sorts of U1 * ()) by ;
then f . e in (doms (F * ())) . e by ;
then f . e in the Sorts of U1 . (() . e) by ;
then g . (f . e) in the Sorts of U2 . (() . e) by ;
hence ((F * ()) .. f) . e in ( the Sorts of U2 * ()) . e by ; :: thesis: verum
end;
(Frege (F * ())) . x = (F * ()) .. f by ;
then (Frege (F * ())) . x in product ( the Sorts of U2 * ()) by ;
hence (Frege (F * ())) . x is Element of Args (o,U2) by PRALG_2:3; :: thesis: verum