let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; :: thesis: for a being non square Element of F holds the carrier of (FAdj (F,{(sqrt a)})) = { (y + ((@ (sqrt a)) * z)) where y, z is F -membered Element of (FAdj (F,{(sqrt a)})) : verum }
let a be non square Element of F; :: thesis: the carrier of (FAdj (F,{(sqrt a)})) = { (y + ((@ (sqrt a)) * z)) where y, z is F -membered Element of (FAdj (F,{(sqrt a)})) : verum }

A: now :: thesis: for o being object st o in the carrier of (FAdj (F,{(sqrt a)})) holds
o in { (y + ((@ (sqrt a)) * z)) where y, z is F -membered Element of (FAdj (F,{(sqrt a)})) : verum }

let o be object ; :: thesis: ( o in the carrier of (FAdj (F,{(sqrt a)})) implies o in { (y + ((@ (sqrt a)) * z)) where y, z is F -membered Element of (FAdj (F,{(sqrt a)})) : verum } )
assume o in the carrier of (FAdj (F,{(sqrt a)})) ; :: thesis: o in { (y + ((@ (sqrt a)) * z)) where y, z is F -membered Element of (FAdj (F,{(sqrt a)})) : verum }
then ex y, z being F -membered Element of (FAdj (F,{(sqrt a)})) st o = y + ((@ (sqrt a)) * z) by qbase2;
hence o in { (y + ((@ (sqrt a)) * z)) where y, z is F -membered Element of (FAdj (F,{(sqrt a)})) : verum } ; :: thesis: verum

end;

now :: thesis: for o being object st o in { (y + ((@ (sqrt a)) * z)) where y, z is F -membered Element of (FAdj (F,{(sqrt a)})) : verum } holds
o in the carrier of (FAdj (F,{(sqrt a)}))

let o be object ; :: thesis: ( o in { (y + ((@ (sqrt a)) * z)) where y, z is F -membered Element of (FAdj (F,{(sqrt a)})) : verum } implies o in the carrier of (FAdj (F,{(sqrt a)})) )
assume o in { (y + ((@ (sqrt a)) * z)) where y, z is F -membered Element of (FAdj (F,{(sqrt a)})) : verum } ; :: thesis: o in the carrier of (FAdj (F,{(sqrt a)}))
then ex y, z being F -membered Element of (FAdj (F,{(sqrt a)})) st o = y + ((@ (sqrt a)) * z) ;
hence o in the carrier of (FAdj (F,{(sqrt a)})) ; :: thesis: verum

end;

hence the carrier of (FAdj (F,{(sqrt a)})) = { (y + ((@ (sqrt a)) * z)) where y, z is F -membered Element of (FAdj (F,{(sqrt a)})) : verum } by A, TARSKI:2; :: thesis: verum