now

let b, c be real number ; :: thesis: ( b |^ n = a & b > 0 & c |^ n = a & c > 0 implies not b <> c )
assume that
A46: ( b |^ n = a & b > 0 ) and
A47: ( c |^ n = a & c > 0 ) and
A48: b <> c ; :: thesis: contradiction

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

suppose b > c ; :: thesis: contradiction

hence contradiction by A1, A46, A47, Lm1; :: thesis: verum

end;

suppose c > b ; :: thesis: contradiction

hence contradiction by A1, A46, A47, 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