let a, b be positive Real; :: thesis: for n being non zero Real holds
( a to_power n = b to_power n iff a = b )
let n be non zero Real; :: thesis: ( a to_power n = b to_power n iff a = b )
( a <> b implies a to_power n <> b to_power n )

proof

assume a <> b ; :: thesis: a to_power n <> b to_power n

per cases then ( a > b or a < b ) by XXREAL_0:1;

suppose B1: a > b ; :: thesis: a to_power n <> b to_power n

per cases ( n > 0 or n < 0 ) ;

suppose n > 0 ; :: thesis: a to_power n <> b to_power n

hence a to_power n <> b to_power n by B1, POWER:37; :: thesis: verum

end;

suppose n < 0 ; :: thesis: a to_power n <> b to_power n

hence a to_power n <> b to_power n by B1, POWER:38; :: thesis: verum

end;

end;

end;

suppose B1: a < b ; :: thesis: a to_power n <> b to_power n

per cases ( n > 0 or n < 0 ) ;

suppose n > 0 ; :: thesis: a to_power n <> b to_power n

hence a to_power n <> b to_power n by B1, POWER:37; :: thesis: verum

end;

suppose n < 0 ; :: thesis: a to_power n <> b to_power n

hence a to_power n <> b to_power n by B1, POWER:38; :: thesis: verum

end;

end;

end;

end;

end;

hence ( a to_power n = b to_power n iff a = b ) ; :: thesis: verum