let R be Ring; :: thesis: for M, N being LeftMod of R
for f, g, h being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,((ADD (M,N)) . (g,h))) = (ADD (M,N)) . (((ADD (M,N)) . (f,g)),h)
let M, N be LeftMod of R; :: thesis: for f, g, h being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,((ADD (M,N)) . (g,h))) = (ADD (M,N)) . (((ADD (M,N)) . (f,g)),h)
let f, g, h be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: (ADD (M,N)) . (f,((ADD (M,N)) . (g,h))) = (ADD (M,N)) . (((ADD (M,N)) . (f,g)),h)
set M1 = the carrier of M;
set N1 = the carrier of N;
reconsider fg = (ADD (M,N)) . (f,g), gh = (ADD (M,N)) . (g,h) as Element of Funcs ( the carrier of M, the carrier of N) ;
set F1 = (ADD (M,N)) . (f,gh);
set F2 = (ADD (M,N)) . (fg,h);
for x being Element of M holds ((ADD (M,N)) . (f,gh)) . x = ((ADD (M,N)) . (fg,h)) . x

proof

let x be Element of M; :: thesis: ((ADD (M,N)) . (f,gh)) . x = ((ADD (M,N)) . (fg,h)) . x
A1: gh . x = (g . x) + (h . x) by Th15;
A2: fg . x = (f . x) + (g . x) by Th15;
((ADD (M,N)) . (f,gh)) . x = (f . x) + ((g . x) + (h . x)) by Th15, A1
.= (fg . x) + (h . x) by A2, RLVECT_1:def 3
.= ((ADD (M,N)) . (fg,h)) . x by Th15 ;
hence ((ADD (M,N)) . (f,gh)) . x = ((ADD (M,N)) . (fg,h)) . x ; :: thesis: verum

end;

hence (ADD (M,N)) . (f,((ADD (M,N)) . (g,h))) = (ADD (M,N)) . (((ADD (M,N)) . (f,g)),h) ; :: thesis: verum