let a, b, f, g 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 )

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

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

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

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

end;

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

then b |^ g = 0 by A2, NAT_1:14, NEWTON:11;
then A8: a = 0 |^ g by A4, A7, CARD_4:3;
b = 0 |^ f by A1, A7, CARD_4:3;
hence ex e being Nat st
( a = e |^ g & b = e |^ f ) by A8; :: thesis: verum

end;

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

consider c, d being Nat such that
A10: (f * c) - (g * d) = 1 by A1, A2, A3, Th31;
reconsider q = (b |^ c) / (a |^ d) as Rational ;
a = a #Z 1 by PREPOWER:35
.= (a |^ (f * c)) / (a |^ (d * g)) by A9, A10, PREPOWER:43
.= ((a |^ f) |^ c) / (a |^ (d * g)) by NEWTON:9
.= ((b |^ g) |^ c) / ((a |^ d) |^ g) by A4, NEWTON:9
.= (b |^ (g * c)) / ((a |^ d) |^ g) by NEWTON:9
.= ((b |^ c) |^ g) / ((a |^ d) |^ g) by NEWTON:9
.= q |^ g by PREPOWER:8 ;
then consider h being Nat such that
A11: a = h |^ g by Th25;
b |^ g = h |^ (f * g) by A4, A11, NEWTON:9
.= (h |^ f) |^ g by NEWTON:9 ;
then b = h |^ f by A2, Th3;
hence ex e being Nat st
( a = e |^ g & b = e |^ f ) by A11; :: thesis: verum

end;

end;

end;

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