let a, b be positive Real; :: thesis: for n being Real holds
( (a + b) to_power n = (a to_power n) + (b to_power n) iff n = 1 )
let n be Real; :: thesis: ( (a + b) to_power n = (a to_power n) + (b to_power n) iff n = 1 )
( (a + b) to_power n = (a to_power n) + (b to_power n) implies n = 1 )

proof

assume A1: (a + b) to_power n = (a to_power n) + (b to_power n) ; :: thesis: n = 1
then A2: ( not n is heavy or not n is positive ) by LME;
reconsider n = n as positive Real by A1, BPC;
( ( n is light & n is positive ) or n = 1 ) by A2, XXREAL_0:1;
hence n = 1 by A1, BPA; :: thesis: verum

end;

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