let it1, it2 be Function of [:COMPLEX,(PFuncs (A,COMPLEX)):],(PFuncs (A,COMPLEX)); ( ( for a being Complex
for f being Element of PFuncs (A,COMPLEX) holds it1 . (a,f) = a (#) f ) & ( for a being Complex
for f being Element of PFuncs (A,COMPLEX) holds it2 . (a,f) = a (#) f ) implies it1 = it2 )
assume that
A2:
for a being Complex
for f being Element of PFuncs (A,COMPLEX) holds it1 . (a,f) = a (#) f
and
A3:
for a being Complex
for f being Element of PFuncs (A,COMPLEX) holds it2 . (a,f) = a (#) f
; it1 = it2
hence
it1 = it2
; verum