/* F[i] := F0(x(i)) */
n*sum(integrate((i/n-u)^2, u, F[i], F[i+1]), i, 0, n) ; /* Origen */
1/(12*n) + sum(((2*i-1)/(2*n)-F[i])^2, i, 1, n) ; /* Destino */

define (sumandoO(i), integrate((i/n-u)^2, u, F[i], F[i+1])) $
sumandoFiO : n*subst ([F[i-1] = 0, F[i+1] = 0], ratsimp(sumandoO(i-1) + sumandoO(i))) ; /* sumando asociado a F[i] */
define (sumandoD(i), ((2*i-1)/(2*n)-F[i])^2) $
sumandoFiD : expand (sumandoD(i)) $
sinFi(x) := freeof (F[i], x) $
conFi(x) := not sinFi(x) $
filtrar (suma, predicado) := apply ("+", sublist (maplist (identity, suma), predicado)) $
sumandoConFi : filtrar (sumandoFiD, conFi) ;
is (factor(sumandoFiO) = factor(sumandoConFi)) ; /* los sumandos en F[i] coinciden */

define (sumandoSinFi(i), filtrar (sumandoFiD, sinFi)) $
TIorigen : ratsimp (nusum (sumandoSinFi(i), i, 1, n) + 1/(12*n)); /* término independiente en Destino */
F[0] : 0 $
F[n+1] : 1 $
sinF(x) := freeof (F, x) $
TIdestino : filtrar (expand (n*sumandoO(n)), sinF) ;
is (TIorigen = TIdestino) ; /* los términos independientes coinciden */