set G = Frege F;
set PD = product (doms F);
set A = (product (doms F)) --> J;
set B = (product (doms F)) --> D;
for i being object 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 object ; :: 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:7;
( i in dom (Frege F) & ((product (doms F)) --> J) . i = J ) by A1, FUNCOP_1:7, PARTFUN1:def 2;
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 15; :: thesis: verum