set V = Funcs ( the carrier of M, the carrier of M);
set V1 = set_End M;
A1: dom (FuncComp M) = [:(Funcs ( the carrier of M, the carrier of M)),(Funcs ( the carrier of M, the carrier of M)):] by FUNCT_2:def 1;
A2: for z being object st z in [:(set_End M),(set_End M):] holds
((FuncComp M) | [:(set_End M),(set_End M):]) . z in set_End M

proof

let z be object ; :: thesis: ( z in [:(set_End M),(set_End M):] implies ((FuncComp M) | [:(set_End M),(set_End M):]) . z in set_End M )
assume A3: z in [:(set_End M),(set_End M):] ; :: thesis: ((FuncComp M) | [:(set_End M),(set_End M):]) . z in set_End M
then consider f, g being object such that
A4: ( f in set_End M & g in set_End M ) and
A5: z = [f,g] by ZFMISC_1:def 2;
reconsider g1 = g, f1 = f as Element of Funcs ( the carrier of M, the carrier of M) by A4;
[f,g] in dom ((FuncComp M) | [:(set_End M),(set_End M):]) by A1, A3, A5, RELAT_1:62, ZFMISC_1:96;
then A6: ((FuncComp M) | [:(set_End M),(set_End M):]) . z = (FuncComp M) . (f1,g1) by A5, FUNCT_1:47;
reconsider f1 = f1, g1 = g1 as additive Function of the carrier of M, the carrier of M by A4, Lm3;
(FuncComp M) . (f1,g1) is additive Function of the carrier of M, the carrier of M by Th5;
hence ((FuncComp M) | [:(set_End M),(set_End M):]) . z in set_End M by A6; :: thesis: verum

end;

dom ((FuncComp M) | [:(set_End M),(set_End M):]) = [:(set_End M),(set_End M):] by A1, RELAT_1:62, ZFMISC_1:96;
hence (FuncComp M) | [:(set_End M),(set_End M):] is BinOp of (set_End M) by A2, FUNCT_2:3; :: thesis: verum