let it1, it2 be Function of [:REAL ,(PFuncs A,REAL ):],(PFuncs A,REAL ); :: thesis: ( ( for a being Real
for f being Element of PFuncs A,REAL holds it1 . a,f = a (#) f ) & ( for a being Real
for f being Element of PFuncs A,REAL holds it2 . a,f = a (#) f ) implies it1 = it2 )
assume that
A1: for a being Real
for f being Element of PFuncs A,REAL holds it1 . a,f = a (#) f and
A2: for a being Real
for f being Element of PFuncs A,REAL holds it2 . a,f = a (#) f ; :: thesis: it1 = it2

now

let a be Element of REAL ; :: thesis: for f being Element of PFuncs A,REAL holds it1 . a,f = it2 . a,f
let f be Element of PFuncs A,REAL ; :: thesis: it1 . a,f = it2 . a,f
thus it1 . a,f = a (#) f by A1
.= it2 . a,f by A2 ; :: thesis: verum

end;

hence it1 = it2 by BINOP_1:2; :: thesis: verum