let a, b be real positive number ; :: thesis: sqrt (((a ^2 ) + (a * b)) + (b ^2 )) = (1 / 2) * (sqrt ((4 * ((a ^2 ) + (b ^2 ))) + ((4 * a) * b)))
A1: ((1 / 2) * (sqrt ((4 * ((a ^2 ) + (b ^2 ))) + ((4 * a) * b)))) ^2 = ((1 / 2) * (1 / 2)) * ((sqrt ((4 * ((a ^2 ) + (b ^2 ))) + ((4 * a) * b))) ^2 )
.= (1 / 4) * ((4 * ((a ^2 ) + (b ^2 ))) + ((4 * a) * b)) by SQUARE_1:def 4
.= (sqrt (((a ^2 ) + (a * b)) + (b ^2 ))) ^2 by SQUARE_1:def 4 ;
A2: sqrt (((a ^2 ) + (a * b)) + (b ^2 )) > 0 by SQUARE_1:93;
sqrt ((4 * ((a ^2 ) + (b ^2 ))) + ((4 * a) * b)) > 0 by SQUARE_1:93;
then sqrt ((sqrt (((a ^2 ) + (a * b)) + (b ^2 ))) ^2 ) = (1 / 2) * (sqrt ((4 * ((a ^2 ) + (b ^2 ))) + ((4 * a) * b))) by A1, SQUARE_1:89;
hence sqrt (((a ^2 ) + (a * b)) + (b ^2 )) = (1 / 2) * (sqrt ((4 * ((a ^2 ) + (b ^2 ))) + ((4 * a) * b))) by A2, SQUARE_1:89; :: thesis: verum