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 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 ;
( 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 }
;
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;
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}))
; verum