A universal coefficient theorem for Gauss's lemma (Q357883)

The authors give a constructive proof of Gauss's lemma in the following form:NEWLINENEWLINEFor any \(m,n\geq1\) there exist polynomials \(c_0,c_1,\dots,c_{m+n}\in Z[X_0,\dots,X_{2(m+n+2)}]\) such that if \(R\) is a commutative ring, and \(a_0,\dots,a_m,b_0,\dots,b_n\in R\) and \(A_0,\dots,A_m,B_0,\dots,B_n\in R\) satisfy NEWLINE\[NEWLINE1=\sum_{i=0}^ma_iA_i=\sum_{j=0}^nb_jB_j,NEWLINE\]NEWLINE then NEWLINE\[NEWLINE\sum_{k=0}^{m+n}c_k(a_0,\dots,b_n,A_0,\dots B_n)C_k = 1NEWLINE\]NEWLINE holds with NEWLINE\[NEWLINEC_k=\sum_{i+j=k}A_iB_j.NEWLINE\]