set V = Funcs ( the carrier of M, the carrier of N);
set V1 = set_Hom (M,N);
A1:
dom (ADD (M,N)) = [:(Funcs ( the carrier of M, the carrier of N)),(Funcs ( the carrier of M, the carrier of N)):]
by FUNCT_2:def 1;
A2:
for z being object st z in [:(set_Hom (M,N)),(set_Hom (M,N)):] holds
((ADD (M,N)) | [:(set_Hom (M,N)),(set_Hom (M,N)):]) . z in set_Hom (M,N)
proof
let z be
object ;
( z in [:(set_Hom (M,N)),(set_Hom (M,N)):] implies ((ADD (M,N)) | [:(set_Hom (M,N)),(set_Hom (M,N)):]) . z in set_Hom (M,N) )
assume A3:
z in [:(set_Hom (M,N)),(set_Hom (M,N)):]
;
((ADD (M,N)) | [:(set_Hom (M,N)),(set_Hom (M,N)):]) . z in set_Hom (M,N)
then consider f,
g being
object such that A4:
(
f in set_Hom (
M,
N) &
g in set_Hom (
M,
N) )
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
N)
by A4;
[f,g] in dom ((ADD (M,N)) | [:(set_Hom (M,N)),(set_Hom (M,N)):])
by A1, A3, A5, RELAT_1:62, ZFMISC_1:96;
then A6:
((ADD (M,N)) | [:(set_Hom (M,N)),(set_Hom (M,N)):]) . z = (ADD (M,N)) . (
f1,
g1)
by A5, FUNCT_1:47;
reconsider f1 =
f1,
g1 =
g1 as
Homomorphism of
R,
M,
N by A4, Lm29;
(ADD (M,N)) . (
f1,
g1) is
Homomorphism of
R,
M,
N
by Th18;
hence
((ADD (M,N)) | [:(set_Hom (M,N)),(set_Hom (M,N)):]) . z in set_Hom (
M,
N)
by A6;
verum
end;
dom ((ADD (M,N)) | [:(set_Hom (M,N)),(set_Hom (M,N)):]) = [:(set_Hom (M,N)),(set_Hom (M,N)):]
by A1, RELAT_1:62, ZFMISC_1:96;
hence
(ADD (M,N)) | [:(set_Hom (M,N)),(set_Hom (M,N)):] is BinOp of (set_Hom (M,N))
by A2, FUNCT_2:3; verum