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

now

let a be Real; :: thesis: for f being Element of Funcs A,REAL holds it1 . a,f = it2 . a,f
let f be Element of Funcs A,REAL ; :: thesis: it1 . a,f = it2 . a,f
thus it1 . a,f = multreal [;] a,f by A2
.= it2 . a,f by A3 ; :: thesis: verum

end;

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