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