set M = { [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } ;
H: FAdj (F,{a}) = RAdj (F,{a}) by FIELD_6:56;
I: FAdj (F,{b}) = RAdj (F,{b}) by FIELD_6:56;

now :: thesis: for o being object st o in { [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } holds
o in [: the carrier of (FAdj (F,{a})), the carrier of (FAdj (F,{b})):]

let o be object ; :: thesis: ( o in { [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } implies o in [: the carrier of (FAdj (F,{a})), the carrier of (FAdj (F,{b})):] )
assume o in { [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } ; :: thesis: o in [: the carrier of (FAdj (F,{a})), the carrier of (FAdj (F,{b})):]
then consider p being Polynomial of F such that
A: o = [(Ext_eval (p,a)),(Ext_eval (p,b))] ;
Ext_eval (p,a) in { (Ext_eval (p,a)) where p is Polynomial of F : verum } ;
then B: Ext_eval (p,a) in the carrier of (FAdj (F,{a})) by H, FIELD_6:45;
Ext_eval (p,b) in { (Ext_eval (p,b)) where p is Polynomial of F : verum } ;
then Ext_eval (p,b) in the carrier of (FAdj (F,{b})) by I, FIELD_6:45;
hence o in [: the carrier of (FAdj (F,{a})), the carrier of (FAdj (F,{b})):] by A, B, ZFMISC_1:def 2; :: thesis: verum

end;

then { [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } c= [: the carrier of (FAdj (F,{a})), the carrier of (FAdj (F,{b})):] ;
hence { [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } is Relation of the carrier of (FAdj (F,{a})), the carrier of (FAdj (F,{b})) ; :: thesis: verum