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 S1[ Nat] means (power (MultGroup R)) . (x,$1) = (power R) . (y,$1);
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[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: S1[ 0 ] by Th17;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A4, A2); :: thesis: verum