let it1, it2 be Function of [:REAL ,(Funcs X,the carrier of Y):],(Funcs X,the carrier of Y); :: thesis: ( ( for a being Real
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (it1 . [a,f]) . x = a * (f . x) ) & ( for a being Real
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (it2 . [a,f]) . x = a * (f . x) ) implies it1 = it2 )
assume that
A1: for a being Real
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (it1 . [a,f]) . x = a * (f . x) and
A2: for a being Real
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (it2 . [a,f]) . x = a * (f . x) ; :: thesis: it1 = it2

now

let a be Element of REAL ; :: thesis: for f being Element of Funcs X,the carrier of Y holds it1 . a,f = it2 . a,f
let f be Element of Funcs X,the carrier of Y; :: thesis: it1 . a,f = it2 . a,f

now

let x be Element of X; :: thesis: (it1 . [a,f]) . x = (it2 . [a,f]) . x
thus (it1 . [a,f]) . x = a * (f . x) by A1
.= (it2 . [a,f]) . x by A2 ; :: thesis: verum

end;

hence it1 . a,f = it2 . a,f by FUNCT_2:113; :: thesis: verum

end;

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