theorem baseZ: :: FIELD_10:55

{1,zeta} is Basis of (VecSp ((FAdj (F_Rat,{zeta})),F_Rat))