H: FAdj (F,{a}) = RAdj (F,{a}) by FIELD_6:56;
A: for o being object st o in dom (Phi (a,b)) holds
o in the carrier of (FAdj (F,{a})) ;

now :: thesis: for o being object st o in the carrier of (FAdj (F,{a})) holds
o in dom (Phi (a,b))

let o be object ; :: thesis: ( o in the carrier of (FAdj (F,{a})) implies o in dom (Phi (a,b)) )
assume o in the carrier of (FAdj (F,{a})) ; :: thesis: o in dom (Phi (a,b))
then o in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by H, FIELD_6:45;
then consider p being Polynomial of F such that
A: o = Ext_eval (p,a) ;
ex y being object st [o,y] in Phi (a,b)

proof

take y = Ext_eval (p,b); :: thesis: [o,y] in Phi (a,b)
thus [o,y] in Phi (a,b) by A; :: thesis: verum

end;

hence o in dom (Phi (a,b)) by XTUPLE_0:def 12; :: thesis: verum

end;

then dom (Phi (a,b)) = the carrier of (FAdj (F,{a})) by A, TARSKI:2;
hence Phi (a,b) is quasi_total by FUNCT_2:def 1; :: thesis: verum