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

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

hence
F1 = F2
; :: thesis: verumlet 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;thus F1 . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) by A5

.= F2 . q by A6 ; :: thesis: verum