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 7
.= ((power R) . (y,k)) * y by A1, A3, Th19
.= (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 Th20;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A2); :: thesis: verum