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

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

let 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;

hence (ComplexFuncExtMult A) . [1r,f] = f by FUNCT_2:63; :: thesis: verum