let X be non empty set ; :: thesis: for Y being RealLinearSpace
for f being Element of Funcs X,the carrier of Y
for a, b being Real holds (FuncExtMult X,Y) . [a,((FuncExtMult X,Y) . [b,f])] = (FuncExtMult X,Y) . [(a * b),f]
let Y be RealLinearSpace; :: thesis: for f being Element of Funcs X,the carrier of Y
for a, b being Real 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 Real holds (FuncExtMult X,Y) . [a,((FuncExtMult X,Y) . [b,f])] = (FuncExtMult X,Y) . [(a * b),f]
let a, b be Real; :: thesis: (FuncExtMult X,Y) . [a,((FuncExtMult X,Y) . [b,f])] = (FuncExtMult X,Y) . [(a * b),f]

now

let x be Element of X; :: thesis: ((FuncExtMult X,Y) . [a,((FuncExtMult X,Y) . [b,f])]) . x = ((FuncExtMult X,Y) . [(a * b),f]) . x
thus ((FuncExtMult X,Y) . [a,((FuncExtMult X,Y) . [b,f])]) . x = a * (((FuncExtMult X,Y) . [b,f]) . x) by Th5
.= a * (b * (f . x)) by Th5
.= (a * b) * (f . x) by RLVECT_1:def 10
.= ((FuncExtMult X,Y) . [(a * b),f]) . x by Th5 ; :: thesis: verum

end;

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