let h be Function; :: thesis: ( dom (Frege <*h*>) = product <*(dom h)*> & rng (Frege <*h*>) = product <*(rng h)*> & ( for x being object st x in dom h holds
(Frege <*h*>) . <*x*> = <*(h . x)*> ) )
A1: <*h*> . 1 = h by FINSEQ_1:def 8;
A2: rngs <*h*> = <*(rng h)*> by Th130;
A3: doms <*h*> = <*(dom h)*> by Th130;
hence ( dom (Frege <*h*>) = product <*(dom h)*> & rng (Frege <*h*>) = product <*(rng h)*> ) by A2, FUNCT_6:38, FUNCT_6:def 7; :: thesis: for x being object st x in dom h holds
(Frege <*h*>) . <*x*> = <*(h . x)*>
let x be object ; :: thesis: ( x in dom h implies (Frege <*h*>) . <*x*> = <*(h . x)*> )
assume x in dom h ; :: thesis: (Frege <*h*>) . <*x*> = <*(h . x)*>
then A4: <*x*> in product (doms <*h*>) by A3, Th121;
then consider f being Function such that
A5: (Frege <*h*>) . <*x*> = f and
dom f = dom <*h*> and
for y being object st y in dom f holds
f . y = (uncurry <*h*>) . (y,(<*x*> . y)) by FUNCT_6:def 7;
A6: ( dom <*h*> = Seg 1 & 1 in Seg 1 ) by FINSEQ_1:2, FINSEQ_1:def 8, TARSKI:def 1;
then ( dom <*(rng h)*> = Seg 1 & f in product (rngs <*h*>) ) by A1, A4, A5, FINSEQ_1:def 8, FUNCT_6:37;
then A7: dom f = Seg 1 by A2, CARD_3:9;
A8: <*x*> . 1 = x by FINSEQ_1:def 8;
reconsider f = f as FinSequence by A7, FINSEQ_1:def 2;
f . 1 = h . (<*x*> . 1) by A6, A1, A4, A5, FUNCT_6:37;
hence (Frege <*h*>) . <*x*> = <*(h . x)*> by A5, A7, A8, FINSEQ_1:def 8; :: thesis: verum