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₁[ Nat] means (power (MultGroup R)) . (x,$1) = (power R) . (y,$1);
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[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;

( (power (MultGroup R)) . (x,0) = 1_ (MultGroup R) & (power R) . (y,0) = 1_ R ) by GROUP_1:def 7;
then A4: S₁[ 0 ] by Th17;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A2); :: thesis: verum