set F = FAdj (F_Rat,{3-CRoot(2),zeta});
set K = FAdj (F_Rat,{3-CRoot(2)});
B: FAdj (F_Rat,{3-CRoot(2)}) = FAdj (F_Rat,{3-Root(2)}) by mmk;
C: FAdj (F_Rat,{3-CRoot(2),zeta}) = FAdj (F_Rat,({3-CRoot(2)} \/ {zeta})) by ENUMSET1:1
.= FAdj ((FAdj (F_Rat,{3-CRoot(2)})),{zeta}) by FIELD_7:35 ;
set M = {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)};
reconsider B1 = {1,3-Root(2),(3-Root(2) ^2)} as Basis of (VecSp ((FAdj (F_Rat,{3-CRoot(2)})),F_Rat)) by B, bas3R;
reconsider B2 = {1,zeta} as Basis of (VecSp ((FAdj (F_Rat,{3-CRoot(2),zeta})),(FAdj (F_Rat,{3-CRoot(2)})))) by baszeta;
E: Base (B1,B2) = { (a * b) where a, b is Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) : ( a in B1 & b in B2 ) } by FIELD_7:def 7;
Base (B1,B2) = {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)}

proof

E1: now :: thesis: for o being object st o in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} holds
o in Base (B1,B2)

let o be object ; :: thesis: ( o in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} implies b₁ in Base (B1,B2) )
assume o in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} ; :: thesis: b₁ in Base (B1,B2)

per cases then ( o = 1 or o = 3-Root(2) or o = 3-Root(2) ^2 or o = zeta or o = 3-Root(2) * zeta or o = (3-Root(2) ^2) * zeta ) by ENUMSET1:def 4;

suppose E0: o = 1 ; :: thesis: b₁ in Base (B1,B2)

set a = 1. (FAdj (F_Rat,{3-CRoot(2),zeta}));
set b = 1. (FAdj (F_Rat,{3-CRoot(2),zeta}));
E1: ( 1. (FAdj (F_Rat,{3-CRoot(2),zeta})) = 1. F_Complex & 1. (FAdj (F_Rat,{3-CRoot(2),zeta})) = 1. F_Complex ) by EC_PF_1:def 1;
then ( 1. (FAdj (F_Rat,{3-CRoot(2),zeta})) = 1 & 1. (FAdj (F_Rat,{3-CRoot(2),zeta})) = 1 ) by COMPLEX1:def 4, COMPLFLD:def 1;
then E2: ( 1. (FAdj (F_Rat,{3-CRoot(2),zeta})) in B1 & 1. (FAdj (F_Rat,{3-CRoot(2),zeta})) in B2 ) by ENUMSET1:def 1, TARSKI:def 2;
(1. (FAdj (F_Rat,{3-CRoot(2),zeta}))) * (1. (FAdj (F_Rat,{3-CRoot(2),zeta}))) = 1 by E1, COMPLEX1:def 4, COMPLFLD:def 1;
hence o in Base (B1,B2) by E, E2, E0; :: thesis: verum

end;

suppose E0: o = 3-Root(2) ; :: thesis: b₁ in Base (B1,B2)

( {3-CRoot(2),zeta} is Subset of (FAdj (F_Rat,{3-CRoot(2),zeta})) & 3-Root(2) in {3-CRoot(2),zeta} ) by TARSKI:def 2, FIELD_6:35;
then reconsider a = 3-Root(2) as Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) ;
set b = 1. (FAdj (F_Rat,{3-CRoot(2),zeta}));
1. (FAdj (F_Rat,{3-CRoot(2),zeta})) = 1. F_Complex by EC_PF_1:def 1
.= 1 by COMPLEX1:def 4, COMPLFLD:def 1 ;
then E1: ( a in B1 & 1. (FAdj (F_Rat,{3-CRoot(2),zeta})) in B2 ) by ENUMSET1:def 1, TARSKI:def 2;
a * (1. (FAdj (F_Rat,{3-CRoot(2),zeta}))) = 3-Root(2) ;
hence o in Base (B1,B2) by E, E1, E0; :: thesis: verum

end;

suppose E0: o = 3-Root(2) ^2 ; :: thesis: b₁ in Base (B1,B2)

( {3-CRoot(2),zeta} is Subset of (FAdj (F_Rat,{3-CRoot(2),zeta})) & 3-CRoot(2) in {3-CRoot(2),zeta} ) by TARSKI:def 2, FIELD_6:35;
then reconsider c = 3-CRoot(2) as Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) ;
FAdj (F_Rat,{3-CRoot(2),zeta}) is Subring of F_Complex by FIELD_5:12;
then A: 3-CRoot(2) * 3-CRoot(2) = c * c by FIELD_6:16;
3-Root(2) ^2 = 3-Root(2) * 3-Root(2) by O_RING_1:def 1
.= 3-CRoot(2) * 3-CRoot(2) ;
then reconsider a = 3-Root(2) ^2 as Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) by A;
set b = 1. (FAdj (F_Rat,{3-CRoot(2),zeta}));
1. (FAdj (F_Rat,{3-CRoot(2),zeta})) = 1. F_Complex by EC_PF_1:def 1
.= 1 by COMPLEX1:def 4, COMPLFLD:def 1 ;
then E1: ( a in B1 & 1. (FAdj (F_Rat,{3-CRoot(2),zeta})) in B2 ) by ENUMSET1:def 1, TARSKI:def 2;
a * (1. (FAdj (F_Rat,{3-CRoot(2),zeta}))) = 3-Root(2) ^2 ;
hence o in Base (B1,B2) by E, E1, E0; :: thesis: verum

end;

suppose E0: o = zeta ; :: thesis: b₁ in Base (B1,B2)

( {3-CRoot(2),zeta} is Subset of (FAdj (F_Rat,{3-CRoot(2),zeta})) & zeta in {3-CRoot(2),zeta} ) by TARSKI:def 2, FIELD_6:35;
then reconsider b = zeta as Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) ;
set a = 1. (FAdj (F_Rat,{3-CRoot(2),zeta}));
1. (FAdj (F_Rat,{3-CRoot(2),zeta})) = 1. F_Complex by EC_PF_1:def 1
.= 1 by COMPLEX1:def 4, COMPLFLD:def 1 ;
then E1: ( 1. (FAdj (F_Rat,{3-CRoot(2),zeta})) in B1 & b in B2 ) by ENUMSET1:def 1, TARSKI:def 2;
(1. (FAdj (F_Rat,{3-CRoot(2),zeta}))) * b = zeta ;
hence o in Base (B1,B2) by E, E1, E0; :: thesis: verum

end;

suppose E0: o = 3-Root(2) * zeta ; :: thesis: b₁ in Base (B1,B2)

( {3-CRoot(2),zeta} is Subset of (FAdj (F_Rat,{3-CRoot(2),zeta})) & zeta in {3-CRoot(2),zeta} & 3-Root(2) in {3-CRoot(2),zeta} ) by TARSKI:def 2, FIELD_6:35;
then reconsider a = 3-Root(2) , b = zeta as Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) ;
E1: ( a in B1 & b in B2 ) by ENUMSET1:def 1, TARSKI:def 2;
FAdj (F_Rat,{3-CRoot(2),zeta}) is Subring of F_Complex by FIELD_5:12;
then a * b = 3-CRoot(2) * zeta by FIELD_6:16;
hence o in Base (B1,B2) by E, E1, E0; :: thesis: verum

end;

suppose E0: o = (3-Root(2) ^2) * zeta ; :: thesis: b₁ in Base (B1,B2)

A: ( {3-CRoot(2),zeta} is Subset of (FAdj (F_Rat,{3-CRoot(2),zeta})) & zeta in {3-CRoot(2),zeta} & 3-Root(2) in {3-CRoot(2),zeta} ) by TARSKI:def 2, FIELD_6:35;
then reconsider c = 3-CRoot(2) as Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) ;
FAdj (F_Rat,{3-CRoot(2),zeta}) is Subring of F_Complex by FIELD_5:12;
then B: 3-CRoot(2) * 3-CRoot(2) = c * c by FIELD_6:16;
C: 3-Root(2) ^2 = 3-Root(2) * 3-Root(2) by O_RING_1:def 1
.= 3-CRoot(2) * 3-CRoot(2) ;
then reconsider a = 3-Root(2) ^2 , b = zeta as Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) by A, B;
E1: ( a in B1 & b in B2 ) by ENUMSET1:def 1, TARSKI:def 2;
FAdj (F_Rat,{3-CRoot(2),zeta}) is Subring of F_Complex by FIELD_5:12;
then a * b = (3-CRoot(2) * 3-CRoot(2)) * zeta by C, FIELD_6:16;
hence o in Base (B1,B2) by C, E, E1, E0; :: thesis: verum

end;

end;

end;

now :: thesis: for o being object st o in Base (B1,B2) holds
o in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)}

let o be object ; :: thesis: ( o in Base (B1,B2) implies b₁ in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} )
assume o in Base (B1,B2) ; :: thesis: b₁ in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)}
then consider a, b being Element of (FAdj (F_Rat,{3-CRoot(2),zeta})) such that
E0: ( o = a * b & a in B1 & b in B2 ) by E;

per cases ( a = 1 or a = 3-Root(2) or a = 3-Root(2) ^2 ) by E0, ENUMSET1:def 1;

suppose E1: a = 1 ; :: thesis: b₁ in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)}

per cases ( b = 1 or b = zeta ) by E0, TARSKI:def 2;

suppose b = 1 ; :: thesis: b₁ in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)}

then E2: ( a = 1. F_Complex & b = 1. F_Complex ) by E1, COMPLEX1:def 4, COMPLFLD:def 1;
FAdj (F_Rat,{3-CRoot(2),zeta}) is Subring of F_Complex by FIELD_5:12;
then a * b = (1. F_Complex) * (1. F_Complex) by E2, FIELD_6:16
.= 1 by COMPLEX1:def 4, COMPLFLD:def 1 ;
hence o in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} by E0, ENUMSET1:def 4; :: thesis: verum

end;

suppose E2: b = zeta ; :: thesis: b₁ in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)}

E3: a = 1. F_Complex by E1, COMPLEX1:def 4, COMPLFLD:def 1;
FAdj (F_Rat,{3-CRoot(2),zeta}) is Subring of F_Complex by FIELD_5:12;
then a * b = (1. F_Complex) * zeta by E2, E3, FIELD_6:16
.= zeta ;
hence o in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} by E0, ENUMSET1:def 4; :: thesis: verum

end;

end;

end;

suppose E1: a = 3-Root(2) ; :: thesis: b₁ in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)}

per cases ( b = 1 or b = zeta ) by E0, TARSKI:def 2;

suppose b = 1 ; :: thesis: b₁ in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)}

then E2: b = 1. F_Complex by COMPLEX1:def 4, COMPLFLD:def 1;
FAdj (F_Rat,{3-CRoot(2),zeta}) is Subring of F_Complex by FIELD_5:12;
then a * b = 3-CRoot(2) * (1. F_Complex) by E1, E2, FIELD_6:16
.= 3-Root(2) ;
hence o in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} by E0, ENUMSET1:def 4; :: thesis: verum

end;

suppose E2: b = zeta ; :: thesis: b₁ in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)}

FAdj (F_Rat,{3-CRoot(2),zeta}) is Subring of F_Complex by FIELD_5:12;
then a * b = 3-CRoot(2) * zeta by E1, E2, FIELD_6:16;
hence o in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} by E0, ENUMSET1:def 4; :: thesis: verum

end;

end;

end;

suppose E1: a = 3-Root(2) ^2 ; :: thesis: b₁ in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)}

per cases ( b = 1 or b = zeta ) by E0, TARSKI:def 2;

suppose b = 1 ; :: thesis: b₁ in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)}

then E2: b = 1. F_Complex by COMPLEX1:def 4, COMPLFLD:def 1;
E3: FAdj (F_Rat,{3-CRoot(2),zeta}) is Subring of F_Complex by FIELD_5:12;
E4: 3-Root(2) ^2 = 3-Root(2) * 3-Root(2) by O_RING_1:def 1
.= 3-CRoot(2) * 3-CRoot(2) ;
then a * b = (3-CRoot(2) * 3-CRoot(2)) * (1. F_Complex) by E1, E2, E3, FIELD_6:16
.= 3-Root(2) ^2 by E4 ;
hence o in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} by E0, ENUMSET1:def 4; :: thesis: verum

end;

suppose E2: b = zeta ; :: thesis: b₁ in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)}

E3: FAdj (F_Rat,{3-CRoot(2),zeta}) is Subring of F_Complex by FIELD_5:12;
E4: 3-Root(2) ^2 = 3-Root(2) * 3-Root(2) by O_RING_1:def 1
.= 3-CRoot(2) * 3-CRoot(2) ;
then a * b = (3-CRoot(2) * 3-CRoot(2)) * zeta by E1, E2, E3, FIELD_6:16
.= (3-Root(2) ^2) * zeta by E4 ;
hence o in {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} by E0, ENUMSET1:def 4; :: thesis: verum

end;

end;

end;

end;

end;

hence Base (B1,B2) = {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} by E1, TARSKI:2; :: thesis: verum

end;

hence {1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} is Basis of (VecSp ((FAdj (F_Rat,{3-CRoot(2),zeta})),F_Rat)) by C, FIELD_7:29; :: thesis: verum