let A be non empty set ; :: thesis: for f being Element of Funcs (A,COMPLEX)

for a, b being Complex holds (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]

let f be Element of Funcs (A,COMPLEX); :: thesis: for a, b being Complex holds (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]

let a, b be Complex; :: thesis: (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]

reconsider a = a, b = b as Element of COMPLEX by XCMPLX_0:def 2;

reconsider ab = a * b as Element of COMPLEX by XCMPLX_0:def 2;

for a, b being Complex holds (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]

let f be Element of Funcs (A,COMPLEX); :: thesis: for a, b being Complex holds (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]

let a, b be Complex; :: thesis: (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]

reconsider a = a, b = b as Element of COMPLEX by XCMPLX_0:def 2;

reconsider ab = a * b as Element of COMPLEX by XCMPLX_0:def 2;

now :: thesis: for x being Element of A holds ((ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])]) . x = ((ComplexFuncExtMult A) . [ab,f]) . x

hence
(ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]
by FUNCT_2:63; :: thesis: verumlet x be Element of A; :: thesis: ((ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])]) . x = ((ComplexFuncExtMult A) . [ab,f]) . x

thus ((ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])]) . x = a * (((ComplexFuncExtMult A) . [b,f]) . x) by Th4

.= a * (b * (f . x)) by Th4

.= (a * b) * (f . x)

.= ((ComplexFuncExtMult A) . [ab,f]) . x by Th4 ; :: thesis: verum

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

.= a * (b * (f . x)) by Th4

.= (a * b) * (f . x)

.= ((ComplexFuncExtMult A) . [ab,f]) . x by Th4 ; :: thesis: verum