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 for o being object st o in the carrier of (FAdj (F,{a})) holds
o in dom (Phi (a,b))let o be
object ;
( o in the carrier of (FAdj (F,{a})) implies o in dom (Phi (a,b)) )assume
o in the
carrier of
(FAdj (F,{a}))
;
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)
hence
o in dom (Phi (a,b))
by XTUPLE_0:def 12;
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; verum