let R be comRing; for S being comRingExtension of R
for x1, x2 being Element of S
for y1, y2 being Element of R
for n being Element of NAT st x1 = y1 & x2 = y2 holds
<%x1,x2%> `^ n = <%y1,y2%> `^ n
let S be comRingExtension of R; for x1, x2 being Element of S
for y1, y2 being Element of R
for n being Element of NAT st x1 = y1 & x2 = y2 holds
<%x1,x2%> `^ n = <%y1,y2%> `^ n
let x1, x2 be Element of S; for y1, y2 being Element of R
for n being Element of NAT st x1 = y1 & x2 = y2 holds
<%x1,x2%> `^ n = <%y1,y2%> `^ n
let y1, y2 be Element of R; for n being Element of NAT st x1 = y1 & x2 = y2 holds
<%x1,x2%> `^ n = <%y1,y2%> `^ n
let n be Element of NAT ; ( x1 = y1 & x2 = y2 implies <%x1,x2%> `^ n = <%y1,y2%> `^ n )
assume A:
( x1 = y1 & x2 = y2 )
; <%x1,x2%> `^ n = <%y1,y2%> `^ n
defpred S1[ Nat] means <%x1,x2%> `^ $1 = <%y1,y2%> `^ $1;
<%x1,x2%> `^ 0 =
1_. S
by POLYNOM5:15
.=
1_. R
by FIELD_4:14
.=
<%y1,y2%> `^ 0
by POLYNOM5:15
;
then IA:
S1[ 0 ]
;
reconsider qS = <%x1,x2%> as Element of the carrier of (Polynom-Ring S) by POLYNOM3:def 10;
reconsider qR = <%y1,y2%> as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
R is Subring of S
by FIELD_4:def 1;
then E:
<%x1,x2%> = <%y1,y2%>
by A, pr20;
IS:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume IV:
S1[
k]
;
S1[k + 1]B:
<%x1,x2%> `^ (k + 1) =
(power (Polynom-Ring S)) . (
<%x1,x2%>,
(k + 1))
by POLYNOM5:def 3
.=
((power (Polynom-Ring S)) . (qS,k)) * qS
by GROUP_1:def 7
;
C:
<%y1,y2%> `^ (k + 1) =
(power (Polynom-Ring R)) . (
<%y1,y2%>,
(k + 1))
by POLYNOM5:def 3
.=
((power (Polynom-Ring R)) . (qR,k)) * qR
by GROUP_1:def 7
;
D:
(power (Polynom-Ring R)) . (
qR,
k) =
<%x1,x2%> `^ k
by IV, POLYNOM5:def 3
.=
(power (Polynom-Ring S)) . (
qS,
k)
by POLYNOM5:def 3
;
reconsider u =
(power (Polynom-Ring R)) . (
qR,
k) as
Polynomial of
R by POLYNOM3:def 10;
reconsider v =
(power (Polynom-Ring S)) . (
qS,
k) as
Polynomial of
S by POLYNOM3:def 10;
((power (Polynom-Ring R)) . (qR,k)) * qR =
u *' <%y1,y2%>
by POLYNOM3:def 10
.=
v *' <%x1,x2%>
by D, E, FIELD_4:17
.=
((power (Polynom-Ring S)) . (qS,k)) * qS
by POLYNOM3:def 10
;
hence
S1[
k + 1]
by B, C;
verum end;
for k being Nat holds S1[k]
from NAT_1:sch 2(IA, IS);
hence
<%x1,x2%> `^ n = <%y1,y2%> `^ n
; verum