let a, b, m be Nat; :: thesis: ( m > 0 implies ex k being Nat st ((a,b) In_Power m) . 1 = a * k )
( m > 0 implies ex k being Nat st ((a,b) In_Power (m + 0)) . (0 + 1) = a * k ) by Th50;
hence ( m > 0 implies ex k being Nat st ((a,b) In_Power m) . 1 = a * k ) ; :: thesis: verum