let R be Skew-Field; :: thesis: for x being Element of ()
for y being Element of R st y = x holds
for k being Nat holds (power ()) . (x,k) = () . (y,k)

let x be Element of (); :: thesis: for y being Element of R st y = x holds
for k being Nat holds (power ()) . (x,k) = () . (y,k)

let y be Element of R; :: thesis: ( y = x implies for k being Nat holds (power ()) . (x,k) = () . (y,k) )
assume A1: y = x ; :: thesis: for k being Nat holds (power ()) . (x,k) = () . (y,k)
defpred S1[ Nat] means (power ()) . (x,\$1) = () . (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 ()) . (x,(k + 1)) = ((power ()) . (x,kk)) * x by GROUP_1:def 7
.= (() . (y,kk)) * y by A1, A3, Th16
.= () . (y,(k + 1)) by GROUP_1:def 7 ; :: thesis: verum
end;
( (power ()) . (x,0) = 1_ () & () . (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