for i being Element of A holds (A --> R) . i is complete Heyting LATTICE ;
then ( product (A --> R) is complete & product (A --> R) is Heyting ) by Th13;
hence R |^ A is Heyting by YELLOW_1:def 5; :: thesis: verum