Two proofs with the aid of "Maple 6" computer-algebra system!
----------------------------Warren D Smith April 2003--------

A COMPUTER-AIDED PROOF THAT 

curl( f X g )  =  f div g - g div f   + (g.grad)(f) - (f.grad)(g)

USING "MAPLE6":

> f := [F1(x,y,z), F2(x,y,z), F3(x,y,z)];
                  f := [F1(x, y, z), F2(x, y, z), F3(x, y, z)]

> g := [G1(x,y,z), G2(x,y,z), G3(x,y,z)];
                  g := [G1(x, y, z), G2(x, y, z), G3(x, y, z)]

> v := [x,y,z];
                                 v := [x, y, z]

> P := evalm( curl( crossprod(f,g), v ) );
[/d             \                           /d             \
[|-- F1(x, y, z)| G2(x, y, z) + F1(x, y, z) |-- G2(x, y, z)|
[\dy            /                           \dy            /

       /d             \                           /d             \
     - |-- F2(x, y, z)| G1(x, y, z) - F2(x, y, z) |-- G1(x, y, z)|
       \dy            /                           \dy            /

       /d             \                           /d             \
     - |-- F3(x, y, z)| G1(x, y, z) - F3(x, y, z) |-- G1(x, y, z)|
       \dz            /                           \dz            /

       /d             \                           /d             \
     + |-- F1(x, y, z)| G3(x, y, z) + F1(x, y, z) |-- G3(x, y, z)|,
       \dz            /                           \dz            /

    /d             \                           /d             \
    |-- F2(x, y, z)| G3(x, y, z) + F2(x, y, z) |-- G3(x, y, z)|
    \dz            /                           \dz            /

       /d             \                           /d             \
     - |-- F3(x, y, z)| G2(x, y, z) - F3(x, y, z) |-- G2(x, y, z)|
       \dz            /                           \dz            /

       /d             \                           /d             \
     - |-- F1(x, y, z)| G2(x, y, z) - F1(x, y, z) |-- G2(x, y, z)|
       \dx            /                           \dx            /

       /d             \                           /d             \
     + |-- F2(x, y, z)| G1(x, y, z) + F2(x, y, z) |-- G1(x, y, z)|,
       \dx            /                           \dx            /

    /d             \                           /d             \
    |-- F3(x, y, z)| G1(x, y, z) + F3(x, y, z) |-- G1(x, y, z)|
    \dx            /                           \dx            /

       /d             \                           /d             \
     - |-- F1(x, y, z)| G3(x, y, z) - F1(x, y, z) |-- G3(x, y, z)|
       \dx            /                           \dx            /

       /d             \                           /d             \
     - |-- F2(x, y, z)| G3(x, y, z) - F2(x, y, z) |-- G3(x, y, z)|
       \dy            /                           \dy            /

       /d             \                           /d             \]
     + |-- F3(x, y, z)| G2(x, y, z) + F3(x, y, z) |-- G2(x, y, z)|]
       \dy            /                           \dy            /]

> 
> Q := evalm( f*diverge(g,v) - g*diverge(f,v) ):

> simplify( evalm( P - Q ) );

[/d             \                           /d             \
[|-- F1(x, y, z)| G2(x, y, z) - F2(x, y, z) |-- G1(x, y, z)|
[\dy            /                           \dy            /

                   /d             \   /d             \
     - F3(x, y, z) |-- G1(x, y, z)| + |-- F1(x, y, z)| G3(x, y, z)
                   \dz            /   \dz            /

                   /d             \               /d             \
     - F1(x, y, z) |-- G1(x, y, z)| + G1(x, y, z) |-- F1(x, y, z)|,
                   \dx            /               \dx            /

    /d             \                           /d             \
    |-- F2(x, y, z)| G3(x, y, z) - F3(x, y, z) |-- G2(x, y, z)|
    \dz            /                           \dz            /

                   /d             \   /d             \
     - F1(x, y, z) |-- G2(x, y, z)| + |-- F2(x, y, z)| G1(x, y, z)
                   \dx            /   \dx            /

                   /d             \               /d             \
     - F2(x, y, z) |-- G2(x, y, z)| + G2(x, y, z) |-- F2(x, y, z)|,
                   \dy            /               \dy            /

    /d             \                           /d             \
    |-- F3(x, y, z)| G1(x, y, z) - F1(x, y, z) |-- G3(x, y, z)|
    \dx            /                           \dx            /

                   /d             \   /d             \
     - F2(x, y, z) |-- G3(x, y, z)| + |-- F3(x, y, z)| G2(x, y, z)
                   \dy            /   \dy            /

                   /d             \               /d             \]
     - F3(x, y, z) |-- G3(x, y, z)| + G3(x, y, z) |-- F3(x, y, z)|]
                   \dz            /               \dz            /]

 and yes this is (g.grad)(f) - (f.grad)(g)  !!

Q.E.D.

*********************************************************************************

A COMPUTER-AIDED PROOF THAT

grad( f . g )  =   X curcl(g) + g X curl(f) +  (g.grad)(f) + (f.grad)(g) 

USING "MAPLE6":


> 
>  f := [F1(x,y,z), F2(x,y,z), F3(x,y,z)];
                  f := [F1(x, y, z), F2(x, y, z), F3(x, y, z)]

>  g := [G1(x,y,z), G2(x,y,z), G3(x,y,z)];
                  g := [G1(x, y, z), G2(x, y, z), G3(x, y, z)]

>  v := [x,y,z];
                                 v := [x, y, z]

> P := evalm( grad( innerprod(f,g), v ) );

     [/d             \                           /d             \
P := [|-- F1(x, y, z)| G1(x, y, z) + F1(x, y, z) |-- G1(x, y, z)|
     [\dx            /                           \dx            /

       /d             \                           /d             \
     + |-- F2(x, y, z)| G2(x, y, z) + F2(x, y, z) |-- G2(x, y, z)|
       \dx            /                           \dx            /

       /d             \                           /d             \
     + |-- F3(x, y, z)| G3(x, y, z) + F3(x, y, z) |-- G3(x, y, z)|,
       \dx            /                           \dx            /

    /d             \                           /d             \
    |-- F1(x, y, z)| G1(x, y, z) + F1(x, y, z) |-- G1(x, y, z)|
    \dy            /                           \dy            /

       /d             \                           /d             \
     + |-- F2(x, y, z)| G2(x, y, z) + F2(x, y, z) |-- G2(x, y, z)|
       \dy            /                           \dy            /

       /d             \                           /d             \
     + |-- F3(x, y, z)| G3(x, y, z) + F3(x, y, z) |-- G3(x, y, z)|,
       \dy            /                           \dy            /

    /d             \                           /d             \
    |-- F1(x, y, z)| G1(x, y, z) + F1(x, y, z) |-- G1(x, y, z)|
    \dz            /                           \dz            /

       /d             \                           /d             \
     + |-- F2(x, y, z)| G2(x, y, z) + F2(x, y, z) |-- G2(x, y, z)|
       \dz            /                           \dz            /

       /d             \                           /d             \]
     + |-- F3(x, y, z)| G3(x, y, z) + F3(x, y, z) |-- G3(x, y, z)|]
       \dz            /                           \dz            /]

> 
> Q := evalm( crossprod(f, curl(g,v)) + crossprod(g, curl(f,v)) );

     [            //d             \   /d             \\
Q := [F2(x, y, z) ||-- G2(x, y, z)| - |-- G1(x, y, z)||
     [            \\dx            /   \dy            //

                   //d             \   /d             \\
     - F3(x, y, z) ||-- G1(x, y, z)| - |-- G3(x, y, z)||
                   \\dz            /   \dx            //

                   //d             \   /d             \\
     + G2(x, y, z) ||-- F2(x, y, z)| - |-- F1(x, y, z)||
                   \\dx            /   \dy            //

                   //d             \   /d             \\
     - G3(x, y, z) ||-- F1(x, y, z)| - |-- F3(x, y, z)||,
                   \\dz            /   \dx            //

                //d             \   /d             \\
    F3(x, y, z) ||-- G3(x, y, z)| - |-- G2(x, y, z)||
                \\dy            /   \dz            //

                   //d             \   /d             \\
     - F1(x, y, z) ||-- G2(x, y, z)| - |-- G1(x, y, z)||
                   \\dx            /   \dy            //

                   //d             \   /d             \\
     + G3(x, y, z) ||-- F3(x, y, z)| - |-- F2(x, y, z)||
                   \\dy            /   \dz            //

                   //d             \   /d             \\
     - G1(x, y, z) ||-- F2(x, y, z)| - |-- F1(x, y, z)||,
                   \\dx            /   \dy            //

                //d             \   /d             \\
    F1(x, y, z) ||-- G1(x, y, z)| - |-- G3(x, y, z)||
                \\dz            /   \dx            //

                   //d             \   /d             \\
     - F2(x, y, z) ||-- G3(x, y, z)| - |-- G2(x, y, z)||
                   \\dy            /   \dz            //

                   //d             \   /d             \\
     + G1(x, y, z) ||-- F1(x, y, z)| - |-- F3(x, y, z)||
                   \\dz            /   \dx            //

                   //d             \   /d             \\]
     - G2(x, y, z) ||-- F3(x, y, z)| - |-- F2(x, y, z)||]
                   \\dy            /   \dz            //]

> 
> simplify(evalm(P-Q));

[/d             \                           /d             \
[|-- F1(x, y, z)| G1(x, y, z) + F1(x, y, z) |-- G1(x, y, z)|
[\dx            /                           \dx            /

                   /d             \               /d             \
     + F2(x, y, z) |-- G1(x, y, z)| + F3(x, y, z) |-- G1(x, y, z)|
                   \dy            /               \dz            /

                   /d             \               /d             \
     + G2(x, y, z) |-- F1(x, y, z)| + G3(x, y, z) |-- F1(x, y, z)|,
                   \dy            /               \dz            /

    /d             \                           /d             \
    |-- F2(x, y, z)| G2(x, y, z) + F2(x, y, z) |-- G2(x, y, z)|
    \dy            /                           \dy            /

                   /d             \               /d             \
     + F3(x, y, z) |-- G2(x, y, z)| + F1(x, y, z) |-- G2(x, y, z)|
                   \dz            /               \dx            /

                   /d             \               /d             \
     + G3(x, y, z) |-- F2(x, y, z)| + G1(x, y, z) |-- F2(x, y, z)|,
                   \dz            /               \dx            /

    /d             \                           /d             \
    |-- F3(x, y, z)| G3(x, y, z) + F3(x, y, z) |-- G3(x, y, z)|
    \dz            /                           \dz            /

                   /d             \               /d             \
     + F1(x, y, z) |-- G3(x, y, z)| + F2(x, y, z) |-- G3(x, y, z)|
                   \dx            /               \dy            /

                   /d             \               /d             \]
     + G1(x, y, z) |-- F3(x, y, z)| + G2(x, y, z) |-- F3(x, y, z)|]
                   \dx            /               \dy            /]

> 
and yes this is (g.grad)(f) + (f.grad)(g)  !!
Q.E.D.

******************************************************************************