now

let b, c be real number ; :: thesis: ( b |^ n = a & b > 0 & c |^ n = a & c > 0 implies not b <> c )
assume that
A36: b |^ n = a and
A37: b > 0 and
A38: c |^ n = a and
A39: c > 0 and
A40: b <> c ; :: thesis: contradiction

per cases ( b > c or c > b ) by A40, XXREAL_0:1;

suppose b > c ; :: thesis: contradiction

hence contradiction by A1, A36, A38, A39, Lm1; :: thesis: verum

end;

suppose c > b ; :: thesis: contradiction

hence contradiction by A1, A36, A37, A38, Lm1; :: thesis: verum

end;

end;

end;

hence for b₁, b₂ being real number holds
( ( a > 0 & b₁ |^ n = a & b₁ > 0 & b₂ |^ n = a & b₂ > 0 implies b₁ = b₂ ) & ( a = 0 & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) ) ; :: thesis: verum