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 Element of 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 Element of NAT holds (power (MultGroup R)) . x,k = (power R) . y,k
let y be Element of R; :: thesis: ( y = x implies for k being Element of NAT holds (power (MultGroup R)) . x,k = (power R) . y,k )
assume A1: y = x ; :: thesis: for k being Element of NAT holds (power (MultGroup R)) . x,k = (power R) . y,k
defpred S₁[ Element of NAT ] means (power (MultGroup R)) . x,$1 = (power R) . y,$1;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
thus (power (MultGroup R)) . x,(k + 1) = ((power (MultGroup R)) . x,k) * x by GROUP_1:def 8
.= ((power R) . y,k) * y by A1, A3, Th19
.= (power R) . y,(k + 1) by GROUP_1:def 8 ; :: thesis: verum

end;

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