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)
thus sqr (R1 - R2) = sqr (R1 + (- R2)) by FINSEQOP:89
.= ((sqr R1) + (2 * (mlt R1,(- R2)))) + (sqr (- R2)) by Th98
.= ((sqr R1) + (2 * (mlt R1,(- R2)))) + (sqr R2) by Th83
.= ((sqr R1) + (2 * (mlt R1,((- 1) * R2)))) + (sqr R2) by Th76
.= ((sqr R1) + (2 * ((- 1) * (mlt R1,R2)))) + (sqr R2) by Th94
.= ((sqr R1) + (((- 1) * 2) * (mlt R1,R2))) + (sqr R2) by Th71
.= ((sqr R1) + ((- 1) * (2 * (mlt R1,R2)))) + (sqr R2) by Th71
.= ((sqr R1) + (- (2 * (mlt R1,R2)))) + (sqr R2) by Th76
.= ((sqr R1) - (2 * (mlt R1,R2))) + (sqr R2) by FINSEQOP:89 ; :: thesis: verum