let A be non empty set ; :: thesis: for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncExtMult A) . [1r,f] = f

let f be Element of Funcs (A,COMPLEX); :: thesis: (ComplexFuncExtMult A) . [1r,f] = f

let f be Element of Funcs (A,COMPLEX); :: thesis: (ComplexFuncExtMult A) . [1r,f] = f

now :: thesis: for x being Element of A holds ((ComplexFuncExtMult A) . [1r,f]) . x = f . x

hence
(ComplexFuncExtMult A) . [1r,f] = f
by FUNCT_2:63; :: thesis: verumlet x be Element of A; :: thesis: ((ComplexFuncExtMult A) . [1r,f]) . x = f . x

thus ((ComplexFuncExtMult A) . [1r,f]) . x = 1r * (f . x) by Th4

.= f . x by COMPLEX1:def 4 ; :: thesis: verum

end;thus ((ComplexFuncExtMult A) . [1r,f]) . x = 1r * (f . x) by Th4

.= f . x by COMPLEX1:def 4 ; :: thesis: verum