let F be non almost_trivial Field; :: thesis: for x being non trivial Element of F
for P being Ring st P = ExField (x,<%(0. F),(1. F)%>) holds
<%(0. F),(1. F)%> in ([#] P) /\ ([#] (Polynom-Ring P))
let x be non trivial Element of F; :: thesis: for P being Ring st P = ExField (x,<%(0. F),(1. F)%>) holds
<%(0. F),(1. F)%> in ([#] P) /\ ([#] (Polynom-Ring P))
let P be Ring; :: thesis: ( P = ExField (x,<%(0. F),(1. F)%>) implies <%(0. F),(1. F)%> in ([#] P) /\ ([#] (Polynom-Ring P)) )
set C = carr (x,<%(0. F),(1. F)%>);
set E = ExField (x,<%(0. F),(1. F)%>);
assume A1: P = ExField (x,<%(0. F),(1. F)%>) ; :: thesis: <%(0. F),(1. F)%> in ([#] P) /\ ([#] (Polynom-Ring P))
<%(0. F),(1. F)%> in {<%(0. F),(1. F)%>} by TARSKI:def 1;
then <%(0. F),(1. F)%> in carr (x,<%(0. F),(1. F)%>) by XBOOLE_0:def 3;
then A2: <%(0. F),(1. F)%> in [#] (ExField (x,<%(0. F),(1. F)%>)) by Def8;

now :: thesis: for n being Element of NAT holds <%(0. F),(1. F)%> . n = <%(0. (ExField (x,<%(0. F),(1. F)%>))),(1. (ExField (x,<%(0. F),(1. F)%>)))%> . n

let n be Element of NAT ; :: thesis: <%(0. F),(1. F)%> . b₁ = <%(0. (ExField (x,<%(0. F),(1. F)%>))),(1. (ExField (x,<%(0. F),(1. F)%>)))%> . b₁

per cases ( n = 0 or n = 1 or n >= 2 ) by NAT_1:23;

suppose A3: n = 0 ; :: thesis: <%(0. F),(1. F)%> . b₁ = <%(0. (ExField (x,<%(0. F),(1. F)%>))),(1. (ExField (x,<%(0. F),(1. F)%>)))%> . b₁

hence <%(0. F),(1. F)%> . n = 0. F by POLYNOM5:38
.= 0. (ExField (x,<%(0. F),(1. F)%>)) by Def8
.= <%(0. (ExField (x,<%(0. F),(1. F)%>))),(1. (ExField (x,<%(0. F),(1. F)%>)))%> . n by A3, POLYNOM5:38 ;
:: thesis: verum

end;

suppose A4: n = 1 ; :: thesis: <%(0. F),(1. F)%> . b₁ = <%(0. (ExField (x,<%(0. F),(1. F)%>))),(1. (ExField (x,<%(0. F),(1. F)%>)))%> . b₁

hence <%(0. F),(1. F)%> . n = 1. F by POLYNOM5:38
.= 1. (ExField (x,<%(0. F),(1. F)%>)) by Def8
.= <%(0. (ExField (x,<%(0. F),(1. F)%>))),(1. (ExField (x,<%(0. F),(1. F)%>)))%> . n by A4, POLYNOM5:38 ;
:: thesis: verum

end;

suppose A5: n >= 2 ; :: thesis: <%(0. F),(1. F)%> . b₁ = <%(0. (ExField (x,<%(0. F),(1. F)%>))),(1. (ExField (x,<%(0. F),(1. F)%>)))%> . b₁

hence <%(0. F),(1. F)%> . n = 0. F by POLYNOM5:38
.= 0. (ExField (x,<%(0. F),(1. F)%>)) by Def8
.= <%(0. (ExField (x,<%(0. F),(1. F)%>))),(1. (ExField (x,<%(0. F),(1. F)%>)))%> . n by A5, POLYNOM5:38 ;
:: thesis: verum

end;

end;

end;

then <%(0. F),(1. F)%> = <%(0. (ExField (x,<%(0. F),(1. F)%>))),(1. (ExField (x,<%(0. F),(1. F)%>)))%> ;
then <%(0. F),(1. F)%> in [#] (Polynom-Ring P) by A1, POLYNOM3:def 10;
hence <%(0. F),(1. F)%> in ([#] P) /\ ([#] (Polynom-Ring P)) by A1, A2, XBOOLE_0:def 4; :: thesis: verum