let i be Nat; :: thesis: for R1, R2 being Element of i -tuples_on REAL holds sqr (R1 + R2) = ((sqr R1) + (2 * (mlt R1,R2))) + (sqr R2)
let R1, R2 be Element of i -tuples_on REAL ; :: thesis: sqr (R1 + R2) = ((sqr R1) + (2 * (mlt R1,R2))) + (sqr R2)

now

let j be Nat; :: thesis: ( j in Seg i implies (sqr (R1 + R2)) . j = (((sqr R1) + (2 * (mlt R1,R2))) + (sqr R2)) . j )
assume j in Seg i ; :: thesis: (sqr (R1 + R2)) . j = (((sqr R1) + (2 * (mlt R1,R2))) + (sqr R2)) . j
set r1r2 = (R1 + R2) . j;
set r1 = R1 . j;
set r2 = R2 . j;
set r1'2 = (sqr R1) . j;
set r2'2 = (sqr R2) . j;
set r1r2a = (mlt R1,R2) . j;
set 2r1r2 = (2 * (mlt R1,R2)) . j;
set r1'22r1r2 = ((sqr R1) + (2 * (mlt R1,R2))) . j;
thus (sqr (R1 + R2)) . j = ((R1 + R2) . j) ^2 by VALUED_1:11
.= ((R1 . j) + (R2 . j)) ^2 by Th27
.= (((R1 . j) ^2 ) + ((2 * (R1 . j)) * (R2 . j))) + ((R2 . j) ^2 )
.= (((sqr R1) . j) + (2 * ((R1 . j) * (R2 . j)))) + ((R2 . j) ^2 ) by VALUED_1:11
.= (((sqr R1) . j) + (2 * ((R1 . j) * (R2 . j)))) + ((sqr R2) . j) by VALUED_1:11
.= (((sqr R1) . j) + (2 * ((mlt R1,R2) . j))) + ((sqr R2) . j) by Th87
.= (((sqr R1) . j) + ((2 * (mlt R1,R2)) . j)) + ((sqr R2) . j) by Th66
.= (((sqr R1) + (2 * (mlt R1,R2))) . j) + ((sqr R2) . j) by Th27
.= (((sqr R1) + (2 * (mlt R1,R2))) + (sqr R2)) . j by Th27 ; :: thesis: verum

end;

hence sqr (R1 + R2) = ((sqr R1) + (2 * (mlt R1,R2))) + (sqr R2) by FINSEQ_2:139; :: thesis: verum