let it1, it2 be Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)); ( ( 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)
; it1 = it2
hence
it1 = it2
; verum