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 set st x in dom f1 & y in dom f2 holds
(Frege <*f1,f2*>) . <*x,y*> = <*(f1 . x),(f2 . y)*> ) )
A1: ( doms <*f1,f2*> = <*(dom f1),(dom f2)*> & rngs <*f1,f2*> = <*(rng f1),(rng f2)*> ) by Th34;
hence ( dom (Frege <*f1,f2*>) = product <*(dom f1),(dom f2)*> & rng (Frege <*f1,f2*>) = product <*(rng f1),(rng f2)*> ) by Def7, Th58; :: thesis: for x, y being set st x in dom f1 & y in dom f2 holds
(Frege <*f1,f2*>) . <*x,y*> = <*(f1 . x),(f2 . y)*>
( len <*f1,f2*> = 2 & len <*(rng f1),(rng f2)*> = 2 ) by FINSEQ_1:61;
then A2: ( dom <*f1,f2*> = Seg 2 & dom <*(rng f1),(rng f2)*> = Seg 2 & 1 in Seg 2 & 2 in Seg 2 & <*f1,f2*> . 1 = f1 & <*f1,f2*> . 2 = f2 ) by FINSEQ_1:4, FINSEQ_1:61, FINSEQ_1:def 3, TARSKI:def 2;
let x, y be set ; :: 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 A3: <*x,y*> in product (doms <*f1,f2*>) by A1, Th2;
then consider f being Function such that
A4: (Frege <*f1,f2*>) . <*x,y*> = f and
( dom f = <*f1,f2*> " (SubFuncs (rng <*f1,f2*>)) & ( for z being set st z in dom f holds
f . z = (uncurry <*f1,f2*>) . z,(<*x,y*> . z) ) ) by Def7;
f in product (rngs <*f1,f2*>) by A2, A3, A4, Th57;
then A5: dom f = Seg 2 by A1, A2, CARD_3:18;
then reconsider f = f as FinSequence by FINSEQ_1:def 2;
( f . 1 = f1 . (<*x,y*> . 1) & f . 2 = f2 . (<*x,y*> . 2) & len f = 2 & <*x,y*> . 1 = x & <*x,y*> . 2 = y ) by A2, A3, A4, A5, Th57, FINSEQ_1:61, FINSEQ_1:def 3;
hence (Frege <*f1,f2*>) . <*x,y*> = <*(f1 . x),(f2 . y)*> by A4, FINSEQ_1:61; :: thesis: verum