let A be non empty set ; for f, g being Element of Funcs (A,COMPLEX)
for a being Complex holds (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]
let f, g be Element of Funcs (A,COMPLEX); for a being Complex holds (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]
let a be Complex; (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]
reconsider a = a as Element of COMPLEX by XCMPLX_0:def 2;
now for x being Element of A holds ((ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g)) . x = ((ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]) . xlet x be
Element of
A;
((ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g)) . x = ((ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]) . xthus ((ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g)) . x =
(((ComplexFuncExtMult A) . [a,f]) . x) * (g . x)
by Th2
.=
(a * (f . x)) * (g . x)
by Th4
.=
a * ((f . x) * (g . x))
.=
a * (((ComplexFuncMult A) . (f,g)) . x)
by Th2
.=
((ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]) . x
by Th4
;
verum end;
hence
(ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]
by FUNCT_2:63; verum