let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; :: thesis: for a being non square Element of F holds Base (sqrt a) = {(1. F),(sqrt a)}
let a be non square Element of F; :: thesis: Base (sqrt a) = {(1. F),(sqrt a)}
MinPoly ((sqrt a),F) = X^2- a by m30;
then A: deg (MinPoly ((sqrt a),F)) = 2 by qua4;
H: F is Subfield of embField (canHomP (X^2- a)) by FIELD_4:7;

B: now :: thesis: for x being object st x in {(1. F),(sqrt a)} holds
x in Base (sqrt a)

let x be object ; :: thesis: ( x in {(1. F),(sqrt a)} implies b₁ in Base (sqrt a) )
assume x in {(1. F),(sqrt a)} ; :: thesis: b₁ in Base (sqrt a)

per cases then ( x = 1. F or x = sqrt a ) by TARSKI:def 2;

suppose x = 1. F ; :: thesis: b₁ in Base (sqrt a)

then x = 1_ (embField (canHomP (X^2- a))) by H, EC_PF_1:def 1
.= (sqrt a) |^ 0 by BINOM:8 ;
hence x in Base (sqrt a) by A; :: thesis: verum

end;

suppose x = sqrt a ; :: thesis: b₁ in Base (sqrt a)

then x = (sqrt a) |^ 1 by BINOM:8;
hence x in Base (sqrt a) by A; :: thesis: verum

end;

end;

end;

now :: thesis: for o being object st o in Base (sqrt a) holds
o in {(1. F),(sqrt a)}

let o be object ; :: thesis: ( o in Base (sqrt a) implies b₁ in {(1. F),(sqrt a)} )
assume o in Base (sqrt a) ; :: thesis: b₁ in {(1. F),(sqrt a)}
then consider n being Element of NAT such that
C1: ( o = (sqrt a) |^ n & n < 2 ) by A;
n is trivial by C1, NAT_2:29;

per cases then ( n = 0 or n = 1 ) by NAT_2:def 1;

suppose n = 0 ; :: thesis: b₁ in {(1. F),(sqrt a)}

then o = 1_ (embField (canHomP (X^2- a))) by C1, BINOM:8
.= 1. F by H, EC_PF_1:def 1 ;
hence o in {(1. F),(sqrt a)} by TARSKI:def 2; :: thesis: verum

end;

suppose n = 1 ; :: thesis: b₁ in {(1. F),(sqrt a)}

then o = sqrt a by C1, BINOM:8;
hence o in {(1. F),(sqrt a)} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence Base (sqrt a) = {(1. F),(sqrt a)} by B, TARSKI:2; :: thesis: verum