let R be Skew-Field; :: thesis: for x being Element of (MultGroup R)

for y being Element of R st y = x holds

for k being Nat holds (power (MultGroup R)) . (x,k) = (power R) . (y,k)

let x be Element of (MultGroup R); :: thesis: for y being Element of R st y = x holds

for k being Nat holds (power (MultGroup R)) . (x,k) = (power R) . (y,k)

let y be Element of R; :: thesis: ( y = x implies for k being Nat holds (power (MultGroup R)) . (x,k) = (power R) . (y,k) )

assume A1: y = x ; :: thesis: for k being Nat holds (power (MultGroup R)) . (x,k) = (power R) . (y,k)

defpred S_{1}[ Nat] means (power (MultGroup R)) . (x,$1) = (power R) . (y,$1);

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

then A4: S_{1}[ 0 ]
by Th17;

thus for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A4, A2); :: thesis: verum

for y being Element of R st y = x holds

for k being Nat holds (power (MultGroup R)) . (x,k) = (power R) . (y,k)

let x be Element of (MultGroup R); :: thesis: for y being Element of R st y = x holds

for k being Nat holds (power (MultGroup R)) . (x,k) = (power R) . (y,k)

let y be Element of R; :: thesis: ( y = x implies for k being Nat holds (power (MultGroup R)) . (x,k) = (power R) . (y,k) )

assume A1: y = x ; :: thesis: for k being Nat holds (power (MultGroup R)) . (x,k) = (power R) . (y,k)

defpred S

A2: for k being Nat st S

S

proof

( (power (MultGroup R)) . (x,0) = 1_ (MultGroup R) & (power R) . (y,0) = 1_ R )
by GROUP_1:def 7;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

thus (power (MultGroup R)) . (x,(k + 1)) = ((power (MultGroup R)) . (x,kk)) * x by GROUP_1:def 7

.= ((power R) . (y,kk)) * y by A1, A3, Th16

.= (power R) . (y,(k + 1)) by GROUP_1:def 7 ; :: thesis: verum

end;assume A3: S

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

thus (power (MultGroup R)) . (x,(k + 1)) = ((power (MultGroup R)) . (x,kk)) * x by GROUP_1:def 7

.= ((power R) . (y,kk)) * y by A1, A3, Th16

.= (power R) . (y,(k + 1)) by GROUP_1:def 7 ; :: thesis: verum

then A4: S

thus for k being Nat holds S