set F = F_Real ;
set a = 2-Root(2) ;
set b = - 2-Root(2);
A: X- 2-Root(2) = rpoly (1,2-Root(2)) by FIELD_9:def 2
.= <%(- 2-Root(2)),(1. F_Real)%> by RING_5:10 ;
B: X- (- 2-Root(2)) = rpoly (1,(- 2-Root(2))) by FIELD_9:def 2
.= <%(- (- 2-Root(2))),(1. F_Real)%> by RING_5:10 ;
C: X- (- 2-Root(2)) = rpoly (1,(- 2-Root(2))) by FIELD_9:def 2
.= X+ 2-Root(2) by FIELD_9:def 3 ;
D: (X- 2-Root(2)) * (X- (- 2-Root(2))) = <%(- 2-Root(2)),(1. F_Real)%> *' <%(- (- 2-Root(2))),(1. F_Real)%> by A, B, POLYNOM3:def 10
.= <%((- 2-Root(2)) * (- (- 2-Root(2)))),(((1. F_Real) * (- (- 2-Root(2)))) + ((1. F_Real) * (- 2-Root(2)))),((1. F_Real) * (1. F_Real))%> by FIELD_9:24
.= <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> ;
H: 2-Root(2) * (- 2-Root(2)) = - ((sqrt 2) * (sqrt 2))
.= - ((sqrt 2) ^2) by SQUARE_1:def 1
.= - ((1. F_Rat) + (1. F_Rat)) by SQUARE_1:def 2, GAUSSINT:def 14 ;
the carrier of (Polynom-Ring F_Rat) c= the carrier of (Polynom-Ring F_Real) by FIELD_4:10;
then X^2-2 in the carrier of (Polynom-Ring F_Real) ;
then reconsider p = X^2-2 as Polynomial of F_Real by POLYNOM3:def 10;
E: dom p = NAT by FUNCT_2:def 1
.= dom <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> holds
<%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . o = p . o

let o be object ; :: thesis: ( o in dom <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> implies <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . b₁ = p . b₁ )
assume o in dom <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> ; :: thesis: <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . b₁ = p . b₁
then reconsider i = o as Element of NAT ;
( i <= 2 implies not not i = 0 & ... & not i = 2 ) ;

per cases then ( i = 0 or i = 1 or i = 2 or i > 2 ) ;

suppose C: i = 0 ; :: thesis: <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . b₁ = p . b₁

then <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . i = 2-Root(2) * (- 2-Root(2)) by FIELD_9:16
.= p . i by C, H, FIELD_9:16 ;
hence <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . o = p . o ; :: thesis: verum

end;

suppose C: i = 1 ; :: thesis: <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . b₁ = p . b₁

then <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . i = (- (- 2-Root(2))) + (- 2-Root(2)) by FIELD_9:16
.= p . i by C, FIELD_9:16, GAUSSINT:def 14 ;
hence <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . o = p . o ; :: thesis: verum

end;

suppose C: i = 2 ; :: thesis: <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . b₁ = p . b₁

then <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . i = 1. F_Real by FIELD_9:16
.= p . i by C, FIELD_9:16, GAUSSINT:def 14 ;
hence <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . o = p . o ; :: thesis: verum

end;

suppose i > 2 ; :: thesis: <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . b₁ = p . b₁

then C1: i >= 2 + 1 by NAT_1:13;
then <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . i = 0. F_Real by FIELD_9:16
.= p . i by C1, FIELD_9:16, GAUSSINT:def 14 ;
hence <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> . o = p . o ; :: thesis: verum

end;

end;

end;

then p = <%(2-Root(2) * (- 2-Root(2))),((- (- 2-Root(2))) + (- 2-Root(2))),(1. F_Real)%> by E
.= (X- 2-Root(2)) * (X+ 2-Root(2)) by C, D ;
hence X^2-2 = (X- 2-Root(2)) * (X+ 2-Root(2)) ; :: thesis: verum