let a, b be positive Real; :: 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 2
.= (sqrt (((a ^2) + (a * b)) + (b ^2))) ^2 by SQUARE_1:def 2 ;
A2: sqrt (((a ^2) + (a * b)) + (b ^2)) > 0 by SQUARE_1:25;
sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b)) > 0 by SQUARE_1:25;
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:22;
hence sqrt (((a ^2) + (a * b)) + (b ^2)) = (1 / 2) * (sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b))) by A2, SQUARE_1:22; :: thesis: verum