First we derive the powerseries for asin(x).  Define two matrix-valued functions:

Since the UL element of nm(1,n) is the nth term ratio of atan(x) and the UR = the first term, nm(1,0) nm(1,1) nm(1,2) ... computes atan(x).  Series-comparing the first five matrices with the claimed infinite product:

(The UL 0 on the LHS is really .)  But [km,nm] are a path-invariant pair:

By induction on k and n, truth on the general unit square implies truth on any infinite rectangle.  The two edges at infinity degenerate, and

(series-testing the RHS:)

is another series for atan(x).  Now suppose

Then

and changing variables in the km matrix:

So, dividing out the radiculus,

Testing the first five matrix terms,

Now we need merely integrate dy.  But the matrix product is linear only in the UR.  We can concentrate y there with a k-dependent "similarity" matrix:

Note that m(0) is the identity, and

The m(k) telescope out of the k product, and we can integrate dy:

We can restore this to canonical form with the "similarity" matrix

Since m(1) ≠ identity, we must take care on the left:

(ignoring an extant 0 times a nascent ∞).  QED/2.
The [km,nm] pair (d1) we just exploited is a special and limiting case of the four dimensional system

Test path-invariance in the i-j, j-k, k-n, and n-i planes:

Given path-invariance, we are free to recoordinatize, replacing each matrix by the appropriate product of itself, the others, and their inverses:

km is too wide, but not after we specialize i and j to 1/2 (losing two dimensions and the im and jm matrices), and shift n and k by -1/2:

The (archaically named) split function "similarity" transforms all matrices ...

... while preserving path invariance:

Now the product,

which computes the sum

equals the product

This is exctly 3/2 times our asin2 identity with y=1/2

QED.
Addendum:  To derive the original atan(x) (d1) pair from the gaussfed0 system, we rename variables (introducing the arbitrary offset a) and discard the im and jm matrices, leaving i and j as free parameters:

Then we contrive the "similarity" matrix that puts x in the UR of nm:

Then we shift k and specialize i and j:

Finally, let a →∞ and put in normal form:

which is where we came in.  --rwg

Created with Wolfram Mathematica 7.0