let X be non empty set ; :: thesis: for Y being ComplexLinearSpace

for f being Element of Funcs (X, the carrier of Y)

for a, b being Complex holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]

let Y be ComplexLinearSpace; :: thesis: for f being Element of Funcs (X, the carrier of Y)

for a, b being Complex holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]

let f be Element of Funcs (X, the carrier of Y); :: thesis: for a, b being Complex holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]

let a, b be Complex; :: thesis: (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]

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

hence (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f] ; :: thesis: verum

for f being Element of Funcs (X, the carrier of Y)

for a, b being Complex holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]

let Y be ComplexLinearSpace; :: thesis: for f being Element of Funcs (X, the carrier of Y)

for a, b being Complex holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]

let f be Element of Funcs (X, the carrier of Y); :: thesis: for a, b being Complex holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]

let a, b be Complex; :: thesis: (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]

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

now :: thesis: for x being Element of X holds ((FuncExtMult (X,Y)) . [a1,((FuncExtMult (X,Y)) . [b1,f])]) . x = ((FuncExtMult (X,Y)) . [ab,f]) . x

then
(FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [ab,f]
by FUNCT_2:63;let x be Element of X; :: thesis: ((FuncExtMult (X,Y)) . [a1,((FuncExtMult (X,Y)) . [b1,f])]) . x = ((FuncExtMult (X,Y)) . [ab,f]) . x

thus ((FuncExtMult (X,Y)) . [a1,((FuncExtMult (X,Y)) . [b1,f])]) . x = a1 * (((FuncExtMult (X,Y)) . [b1,f]) . x) by Th2

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

.= (a * b) * (f . x) by CLVECT_1:def 4

.= ((FuncExtMult (X,Y)) . [ab,f]) . x by Th2 ; :: thesis: verum

end;thus ((FuncExtMult (X,Y)) . [a1,((FuncExtMult (X,Y)) . [b1,f])]) . x = a1 * (((FuncExtMult (X,Y)) . [b1,f]) . x) by Th2

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

.= (a * b) * (f . x) by CLVECT_1:def 4

.= ((FuncExtMult (X,Y)) . [ab,f]) . x by Th2 ; :: thesis: verum

hence (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f] ; :: thesis: verum