let f, g, a, b be Nat; :: thesis: ( f > 0 & g > 0 & f gcd g = 1 & a |^ f = b |^ g implies ex e being Nat st
( a = e |^ g & b = e |^ f ) )
assume A1: ( f > 0 & g > 0 & f gcd g = 1 & a |^ f = b |^ g ) ; :: thesis: ex e being Nat st
( a = e |^ g & b = e |^ f )
X: ( a in REAL & b in REAL ) by XREAL_0:def 1;

now

per cases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;

suppose A2: a = 0 ; :: thesis: ex e being Nat st
( a = e |^ g & b = e |^ f )

then a |^ f = 0 by A1, NAT_1:14, NEWTON:16;
then ( a = 0 |^ g & b = 0 |^ f ) by A1, A2, X, CARD_4:51;
hence ex e being Nat st
( a = e |^ g & b = e |^ f ) ; :: thesis: verum

end;

suppose A3: b = 0 ; :: thesis: ex e being Nat st
( a = e |^ g & b = e |^ f )

then b |^ g = 0 by A1, NAT_1:14, NEWTON:16;
then ( a = 0 |^ g & b = 0 |^ f ) by A1, A3, X, CARD_4:51;
hence ex e being Nat st
( a = e |^ g & b = e |^ f ) ; :: thesis: verum

end;

suppose A4: ( a <> 0 & b <> 0 ) ; :: thesis: ex e being Nat st
( a = e |^ g & b = e |^ f )

consider c, d being Nat such that
A5: (f * c) - (g * d) = 1 by A1, Th38;
reconsider q = (b |^ c) / (a |^ d) as Rational ;
a = a #Z 1 by PREPOWER:45
.= (a |^ (f * c)) / (a |^ (d * g)) by A4, A5, PREPOWER:53
.= ((a |^ f) |^ c) / (a |^ (d * g)) by NEWTON:14
.= ((b |^ g) |^ c) / ((a |^ d) |^ g) by A1, NEWTON:14
.= (b |^ (g * c)) / ((a |^ d) |^ g) by NEWTON:14
.= ((b |^ c) |^ g) / ((a |^ d) |^ g) by NEWTON:14
.= q |^ g by PREPOWER:15 ;
then consider h being Nat such that
A6: a = h |^ g by Th32;
b |^ g = h |^ (f * g) by A1, A6, NEWTON:14
.= (h |^ f) |^ g by NEWTON:14 ;
then b = h |^ f by A1, Th5;
hence ex e being Nat st
( a = e |^ g & b = e |^ f ) by A6; :: thesis: verum

end;

end;

end;

hence ex e being Nat st
( a = e |^ g & b = e |^ f ) ; :: thesis: verum