set F = FAdj (F_Rat,{sqrt(-3)});
A: F_Rat is Subfield of FAdj (F_Rat,{sqrt(-3)}) by FIELD_6:36;
{zeta} is Subset of (FAdj (F_Rat,{sqrt(-3)}))

proof

now :: thesis: for o being object st o in {zeta} holds
o in the carrier of (FAdj (F_Rat,{sqrt(-3)}))

let o be object ; :: thesis: ( o in {zeta} implies o in the carrier of (FAdj (F_Rat,{sqrt(-3)})) )
assume o in {zeta} ; :: thesis: o in the carrier of (FAdj (F_Rat,{sqrt(-3)}))
then B1: o = zeta by TARSKI:def 1;
B2: {sqrt(-3)} is Subset of (FAdj (F_Rat,{sqrt(-3)})) by FIELD_6:35;
sqrt(-3) in {sqrt(-3)} by TARSKI:def 1;
then reconsider sqt = sqrt(-3) as Element of (FAdj (F_Rat,{sqrt(-3)})) by B2;
B3: FAdj (F_Rat,{sqrt(-3)}) is Subring of F_Complex by FIELD_5:12;
then B4: ( 1. F_Complex = 1. (FAdj (F_Rat,{sqrt(-3)})) & 1 = 1. F_Complex ) by COMPLEX1:def 4, COMPLFLD:def 1, C0SP1:def 3;
then B5: ( - (1. F_Complex) = - (1. (FAdj (F_Rat,{sqrt(-3)}))) & - 1 = - (1. F_Complex) ) by B3, FIELD_6:17, COMPLFLD:2;
B6: ( (- 1) + (<i> * (sqrt 3)) = (- (1. F_Complex)) + sqrt(-3) & (- (1. F_Complex)) + sqrt(-3) = (- (1. (FAdj (F_Rat,{sqrt(-3)})))) + sqt ) by B3, B5, FIELD_6:15;
set t = (1. F_Complex) + (1. F_Complex);
B9: ((1. F_Complex) + (1. F_Complex)) " = 2 " by B4, COMPLFLD:5, COMPLFLD:9;
B10: (1. F_Complex) + (1. F_Complex) = (1. (FAdj (F_Rat,{sqrt(-3)}))) + (1. (FAdj (F_Rat,{sqrt(-3)}))) by B4, B3, FIELD_6:15;
not (1. F_Complex) + (1. F_Complex) is zero by COMPLFLD:9;
then B11: ((1. F_Complex) + (1. F_Complex)) " = ((1. (FAdj (F_Rat,{sqrt(-3)}))) + (1. (FAdj (F_Rat,{sqrt(-3)})))) " by B10, FIELD_6:18;
((- 1) + (<i> * (sqrt 3))) * (2 ") = ((- (1. F_Complex)) + sqrt(-3)) * (((1. F_Complex) + (1. F_Complex)) ") by B9, B4, COMPLFLD:2
.= ((- (1. (FAdj (F_Rat,{sqrt(-3)})))) + sqt) * (((1. (FAdj (F_Rat,{sqrt(-3)}))) + (1. (FAdj (F_Rat,{sqrt(-3)})))) ") by B3, B6, B11, FIELD_6:16 ;
hence o in the carrier of (FAdj (F_Rat,{sqrt(-3)})) by B1; :: thesis: verum

end;

hence {zeta} is Subset of (FAdj (F_Rat,{sqrt(-3)})) by TARSKI:def 3; :: thesis: verum

end;

then C: FAdj (F_Rat,{zeta}) is Subfield of FAdj (F_Rat,{sqrt(-3)}) by A, FIELD_6:37;
set F = FAdj (F_Rat,{zeta});
A: F_Rat is Subfield of FAdj (F_Rat,{zeta}) by FIELD_6:36;
{sqrt(-3)} is Subset of (FAdj (F_Rat,{zeta}))

proof

now :: thesis: for o being object st o in {sqrt(-3)} holds
o in the carrier of (FAdj (F_Rat,{zeta}))

let o be object ; :: thesis: ( o in {sqrt(-3)} implies o in the carrier of (FAdj (F_Rat,{zeta})) )
assume o in {sqrt(-3)} ; :: thesis: o in the carrier of (FAdj (F_Rat,{zeta}))
then B1: o = sqrt(-3) by TARSKI:def 1;
B2: {zeta} is Subset of (FAdj (F_Rat,{zeta})) by FIELD_6:35;
zeta in {zeta} by TARSKI:def 1;
then reconsider zet = zeta as Element of (FAdj (F_Rat,{zeta})) by B2;
B3: FAdj (F_Rat,{zeta}) is Subring of F_Complex by FIELD_5:12;
then B4: ( 1. F_Complex = 1. (FAdj (F_Rat,{zeta})) & 1 = 1. F_Complex ) by COMPLEX1:def 4, COMPLFLD:def 1, C0SP1:def 3;
set t = (1. F_Complex) + (1. F_Complex);
(1. F_Complex) + (1. F_Complex) = (1. (FAdj (F_Rat,{zeta}))) + (1. (FAdj (F_Rat,{zeta}))) by B3, B4, FIELD_6:15;
then ((1. F_Complex) + (1. F_Complex)) * zeta = ((1. (FAdj (F_Rat,{zeta}))) + (1. (FAdj (F_Rat,{zeta})))) * zet by B3, FIELD_6:16;
then (((1. F_Complex) + (1. F_Complex)) * zeta) + (1. F_Complex) = (((1. (FAdj (F_Rat,{zeta}))) + (1. (FAdj (F_Rat,{zeta})))) * zet) + (1. (FAdj (F_Rat,{zeta}))) by B3, B4, FIELD_6:15;
hence o in the carrier of (FAdj (F_Rat,{zeta})) by B1, B4; :: thesis: verum

end;

hence {sqrt(-3)} is Subset of (FAdj (F_Rat,{zeta})) by TARSKI:def 3; :: thesis: verum

end;

then FAdj (F_Rat,{sqrt(-3)}) is Subfield of FAdj (F_Rat,{zeta}) by A, FIELD_6:37;
hence FAdj (F_Rat,{zeta}) = FAdj (F_Rat,{sqrt(-3)}) by C, FIELD_7:def 2, FIELD_7:2; :: thesis: verum