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 :: thesis: for a being Element of REAL
for f being Element of Funcs (A,REAL) holds it1 . (a,f) = it2 . (a,f)

let a be Element of 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 ; :: thesis: verum