set G = Frege F;
set PD = product (doms F);
set A = (product (doms F)) --> J;
set B = (product (doms F)) --> D;
for i being set st i in product (doms F) holds
(Frege F) . i is Function of ((product (doms F)) --> J) . i,((product (doms F)) --> D) . i

proof

let i be set ; :: thesis: ( i in product (doms F) implies (Frege F) . i is Function of ((product (doms F)) --> J) . i,((product (doms F)) --> D) . i )
assume A1: i in product (doms F) ; :: thesis: (Frege F) . i is Function of ((product (doms F)) --> J) . i,((product (doms F)) --> D) . i
then reconsider f = i as Function ;
A2: ((product (doms F)) --> D) . i = D by A1, FUNCOP_1:13;
( i in dom (Frege F) & ((product (doms F)) --> J) . i = J ) by A1, FUNCOP_1:13, PARTFUN1:def 4;
then (Frege F) . f is Function of ((product (doms F)) --> J) . i,((product (doms F)) --> D) . i by A2, Th10;
hence (Frege F) . i is Function of ((product (doms F)) --> J) . i,((product (doms F)) --> D) . i ; :: thesis: verum

end;

hence Frege F is DoubleIndexedSet of (product (doms F)) --> J,D by PBOOLE:def 18; :: thesis: verum