let it1, it2 be Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)); :: thesis: ( ( for z being Complex
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (it1 . [z,f]) . x = z * (f . x) ) & ( for z being Complex
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (it2 . [z,f]) . x = z * (f . x) ) implies it1 = it2 )
assume that
A2: for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (it1 . [z,f]) . x = z * (f . x) and
A3: for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (it2 . [z,f]) . x = z * (f . x) ; :: thesis: it1 = it2

now

let z be Element of COMPLEX ; :: thesis: for f being Element of Funcs (A,COMPLEX) holds it1 . (z,f) = it2 . (z,f)
let f be Element of Funcs (A,COMPLEX); :: thesis: it1 . (z,f) = it2 . (z,f)

now

let x be Element of A; :: thesis: (it1 . [z,f]) . x = (it2 . [z,f]) . x
thus (it1 . [z,f]) . x = z * (f . x) by A2
.= (it2 . [z,f]) . x by A3 ; :: thesis: verum

end;

hence it1 . (z,f) = it2 . (z,f) by FUNCT_2:63; :: thesis: verum

end;

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