now :: thesis: for b, c being Real st b |^ n = a & b > 0 & c |^ n = a & c > 0 holds
not b <> c

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

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

suppose b > c ; :: thesis: contradiction

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

end;

suppose c > b ; :: thesis: contradiction

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

end;

end;

end;

hence for b₁, b₂ being Real 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