let a, b be Real; :: thesis: ( 4 = 2 |^ 2 & (a + b) |^ 2 = ((a |^ 2) + ((2 * a) * b)) + (b |^ 2) )
A1: (a + b) |^ (1 + 1) = ((a + b) |^ 1) * (a + b) by NEWTON:6
.= (a + b) * (a + b)
.= ((a * a) + (a * b)) + ((a * b) + (b * b))
.= ((a * a) + (a * b)) + ((a * b) + (b |^ 2)) by WSIERP_1:1
.= ((a |^ 2) + (a * b)) + ((a * b) + (b |^ 2)) by WSIERP_1:1
.= ((a |^ 2) + (2 * (a * b))) + (b |^ 2) ;
2 |^ 2 = 2 * 2 by WSIERP_1:1
.= 4 ;
hence ( 4 = 2 |^ 2 & (a + b) |^ 2 = ((a |^ 2) + ((2 * a) * b)) + (b |^ 2) ) by A1; :: thesis: verum