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 that
A1: f > 0 and
A2: g > 0 and
A3: f gcd g = 1 and
A4: a |^ f = b |^ g ; :: thesis: ex e being Nat st
( a = e |^ g & b = e |^ f )
A5: b in REAL by XREAL_0:def 1;
A6: a in REAL by XREAL_0:def 1;

now

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

suppose A7: 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 A8: b = 0 |^ f by A4, A5, A7, CARD_4:51;
a = 0 |^ g by A2, A7, CARD_4:51;
hence ex e being Nat st
( a = e |^ g & b = e |^ f ) by A8; :: thesis: verum

end;

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

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

end;

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

consider c, d being Nat such that
A12: (f * c) - (g * d) = 1 by A1, A2, A3, Th38;
reconsider q = (b |^ c) / (a |^ d) as Rational ;
a = a #Z 1 by PREPOWER:45
.= (a |^ (f * c)) / (a |^ (d * g)) by A11, A12, PREPOWER:53
.= ((a |^ f) |^ c) / (a |^ (d * g)) by NEWTON:14
.= ((b |^ g) |^ c) / ((a |^ d) |^ g) by A4, 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
A13: a = h |^ g by Th32;
b |^ g = h |^ (f * g) by A4, A13, NEWTON:14
.= (h |^ f) |^ g by NEWTON:14 ;
then b = h |^ f by A2, Th5;
hence ex e being Nat st
( a = e |^ g & b = e |^ f ) by A13; :: thesis: verum

end;

end;

end;

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