let F, G be Function of (FAdj (F1,{a})),(FAdj (F2,{b})); :: thesis: ( ( for r being Element of the carrier of (Polynom-Ring F1) holds F . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) ) & ( for r being Element of the carrier of (Polynom-Ring F1) holds G . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) ) implies F = G )
assume that
A1: for r being Element of the carrier of (Polynom-Ring F1) holds F . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) and
A2: for r being Element of the carrier of (Polynom-Ring F1) holds G . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) ; :: thesis: F = G

now :: thesis: for o being object st o in the carrier of (FAdj (F1,{a})) holds
F . o = G . o

let o be object ; :: thesis: ( o in the carrier of (FAdj (F1,{a})) implies F . o = G . o )
assume A3: o in the carrier of (FAdj (F1,{a})) ; :: thesis: F . o = G . o
A4: FAdj (F1,{a}) = RAdj (F1,{a}) by AS, FIELD_6:43, FIELD_6:56;
the carrier of (RAdj (F1,{a})) = { (Ext_eval (p,a)) where p is Polynomial of F1 : verum } by FIELD_6:45;
then consider r being Polynomial of F1 such that
A5: o = Ext_eval (r,a) by A3, A4;
reconsider r = r as Element of the carrier of (Polynom-Ring F1) by POLYNOM3:def 10;
F . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) by A1
.= G . (Ext_eval (r,a)) by A2 ;
hence F . o = G . o by A5; :: thesis: verum

end;

hence F = G ; :: thesis: verum