let S be Ring; :: thesis: for R being Subring of S
for x1, x2 being Element of S
for y1, y2 being Element of R st x1 = y1 & x2 = y2 holds
<%x1,x2%> = <%y1,y2%>
let R be Subring of S; :: thesis: for x1, x2 being Element of S
for y1, y2 being Element of R st x1 = y1 & x2 = y2 holds
<%x1,x2%> = <%y1,y2%>
let x1, x2 be Element of S; :: thesis: for y1, y2 being Element of R st x1 = y1 & x2 = y2 holds
<%x1,x2%> = <%y1,y2%>
let y1, y2 be Element of R; :: thesis: ( x1 = y1 & x2 = y2 implies <%x1,x2%> = <%y1,y2%> )
assume AS: ( x1 = y1 & x2 = y2 ) ; :: thesis: <%x1,x2%> = <%y1,y2%>
set p = <%x1,x2%>;
set q = <%y1,y2%>;
now :: thesis: for n being Element of NAT holds <%x1,x2%> . n = <%y1,y2%> . n
let n be Element of NAT ; :: thesis: <%x1,x2%> . b1 = <%y1,y2%> . b1
per cases ( n is trivial or not n is trivial ) ;
suppose A: n is trivial ; :: thesis: <%x1,x2%> . b1 = <%y1,y2%> . b1
per cases ( n = 0 or n = 1 ) by A, NAT_2:def 1;
suppose B: n = 0 ; :: thesis: <%x1,x2%> . b1 = <%y1,y2%> . b1
hence <%x1,x2%> . n = y1 by AS, POLYNOM5:38
.= <%y1,y2%> . n by B, POLYNOM5:38 ;
:: thesis: verum
end;
suppose B: n = 1 ; :: thesis: <%x1,x2%> . b1 = <%y1,y2%> . b1
hence <%x1,x2%> . n = y2 by AS, POLYNOM5:38
.= <%y1,y2%> . n by B, POLYNOM5:38 ;
:: thesis: verum
end;
end;
end;
suppose A: not n is trivial ; :: thesis: <%x1,x2%> . b1 = <%y1,y2%> . b1
hence <%x1,x2%> . n = 0. S by NAT_2:29, POLYNOM5:38
.= 0. R by C0SP1:def 3
.= <%y1,y2%> . n by A, NAT_2:29, POLYNOM5:38 ;
:: thesis: verum
end;
end;
end;
hence <%x1,x2%> = <%y1,y2%> ; :: thesis: verum