set R = Polynom-Ring p;
let F1, F2 be Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)); :: thesis: ( ( for q being Element of the carrier of (Polynom-Ring p) holds F1 . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) ) & ( for q being Element of the carrier of (Polynom-Ring p) holds F2 . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) ) implies F1 = F2 )
assume that
A5: for q being Element of (Polynom-Ring p) holds F1 . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) and
A6: for q being Element of (Polynom-Ring p) holds F2 . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) ; :: thesis: F1 = F2

now :: thesis: for q being Element of (Polynom-Ring p) holds F1 . q = F2 . q

let q be Element of (Polynom-Ring p); :: thesis: F1 . q = F2 . q
thus F1 . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) by A5
.= F2 . q by A6 ; :: thesis: verum

end;

hence F1 = F2 ; :: thesis: verum