let X be non empty set ; :: thesis: for Y being RealLinearSpace
for f, g being Element of Funcs X,the carrier of Y
for a being Real holds (FuncAdd X,Y) . ((FuncExtMult X,Y) . [a,f]),((FuncExtMult X,Y) . [a,g]) = (FuncExtMult X,Y) . [a,((FuncAdd X,Y) . f,g)]
let Y be RealLinearSpace; :: thesis: for f, g being Element of Funcs X,the carrier of Y
for a being Real holds (FuncAdd X,Y) . ((FuncExtMult X,Y) . [a,f]),((FuncExtMult X,Y) . [a,g]) = (FuncExtMult X,Y) . [a,((FuncAdd X,Y) . f,g)]
let f, g be Element of Funcs X,the carrier of Y; :: thesis: for a being Real holds (FuncAdd X,Y) . ((FuncExtMult X,Y) . [a,f]),((FuncExtMult X,Y) . [a,g]) = (FuncExtMult X,Y) . [a,((FuncAdd X,Y) . f,g)]
let a be Real; :: thesis: (FuncAdd X,Y) . ((FuncExtMult X,Y) . [a,f]),((FuncExtMult X,Y) . [a,g]) = (FuncExtMult X,Y) . [a,((FuncAdd X,Y) . f,g)]

now

let x be Element of X; :: thesis: ((FuncAdd X,Y) . ((FuncExtMult X,Y) . [a,f]),((FuncExtMult X,Y) . [a,g])) . x = ((FuncExtMult X,Y) . [a,((FuncAdd X,Y) . f,g)]) . x
thus ((FuncAdd X,Y) . ((FuncExtMult X,Y) . [a,f]),((FuncExtMult X,Y) . [a,g])) . x = (((FuncExtMult X,Y) . [a,f]) . x) + (((FuncExtMult X,Y) . [a,g]) . x) by Th3
.= (a * (f . x)) + (((FuncExtMult X,Y) . [a,g]) . x) by Th5
.= (a * (f . x)) + (a * (g . x)) by Th5
.= a * ((f . x) + (g . x)) by RLVECT_1:def 8
.= a * (((FuncAdd X,Y) . f,g) . x) by Th3
.= ((FuncExtMult X,Y) . [a,((FuncAdd X,Y) . f,g)]) . x by Th5 ; :: thesis: verum

end;

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