let R be Skew-Field; :: thesis: for n being Nat
for a being Element of R
for b being Element of (MultGroup R) st a = b holds
a |^ n = b |^ n
let n be Nat; :: thesis: for a being Element of R
for b being Element of (MultGroup R) st a = b holds
a |^ n = b |^ n
let a be Element of R; :: thesis: for b being Element of (MultGroup R) st a = b holds
a |^ n = b |^ n
let b be Element of (MultGroup R); :: thesis: ( a = b implies a |^ n = b |^ n )
set M = MultGroup R;
assume AS: a = b ; :: thesis: a |^ n = b |^ n
defpred S₁[ Nat] means for a being Element of R
for b being Element of (MultGroup R) st a = b holds
a |^ $1 = b |^ $1;
IA: S₁[ 0 ]

proof

now :: thesis: for a being Element of R
for b being Element of (MultGroup R) holds a |^ 0 = b |^ 0

let a be Element of R; :: thesis: for b being Element of (MultGroup R) holds a |^ 0 = b |^ 0
let b be Element of (MultGroup R); :: thesis: a |^ 0 = b |^ 0
thus a |^ 0 = 1_ R by BINOM:8
.= 1_ (MultGroup R) by UNIROOTS:17
.= b |^ 0 by GROUP_1:25 ; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for a being Element of R
for b being Element of (MultGroup R) st a = b holds
a |^ (k + 1) = b |^ (k + 1)

let a be Element of R; :: thesis: for b being Element of (MultGroup R) st a = b holds
a |^ (k + 1) = b |^ (k + 1)
let b be Element of (MultGroup R); :: thesis: ( a = b implies a |^ (k + 1) = b |^ (k + 1) )
assume B: a = b ; :: thesis: a |^ (k + 1) = b |^ (k + 1)
then C: a |^ k = b |^ k by A;
thus a |^ (k + 1) = (a |^ k) * (a |^ 1) by BINOM:10
.= (a |^ k) * a by BINOM:8
.= (b |^ k) * b by B, C, UNIROOTS:16
.= b |^ (k + 1) by GROUP_1:34 ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence a |^ n = b |^ n by AS; :: thesis: verum