set CR = the carrier of R;
set V = Funcs ( the carrier of M, the carrier of N);
set V1 = set_Hom (M,N);
A1:
dom (LMULT (M,N)) = [: the carrier of R,(Funcs ( the carrier of M, the carrier of N)):]
by FUNCT_2:def 1;
A2:
for z being object st z in [: the carrier of R,(set_Hom (M,N)):] holds
((LMULT (M,N)) | [: the carrier of R,(set_Hom (M,N)):]) . z in set_Hom (M,N)
proof
let z be
object ;
( z in [: the carrier of R,(set_Hom (M,N)):] implies ((LMULT (M,N)) | [: the carrier of R,(set_Hom (M,N)):]) . z in set_Hom (M,N) )
assume A3:
z in [: the carrier of R,(set_Hom (M,N)):]
;
((LMULT (M,N)) | [: the carrier of R,(set_Hom (M,N)):]) . z in set_Hom (M,N)
then consider a,
g being
object such that A4:
(
a in the
carrier of
R &
g in set_Hom (
M,
N) )
and A5:
z = [a,g]
by ZFMISC_1:def 2;
reconsider a1 =
a as
Element of the
carrier of
R by A4;
reconsider g1 =
g as
Element of
Funcs ( the
carrier of
M, the
carrier of
N)
by A4;
[a1,g1] in dom ((LMULT (M,N)) | [: the carrier of R,(set_Hom (M,N)):])
by A1, A3, A5, RELAT_1:62, ZFMISC_1:96;
then A6:
((LMULT (M,N)) | [: the carrier of R,(set_Hom (M,N)):]) . z = (LMULT (M,N)) . (
a1,
g1)
by A5, FUNCT_1:47;
reconsider g1 =
g1 as
Homomorphism of
R,
M,
N by A4, Lm29;
(LMULT (M,N)) . (
a1,
g1) is
Homomorphism of
R,
M,
N
by Th20;
hence
((LMULT (M,N)) | [: the carrier of R,(set_Hom (M,N)):]) . z in set_Hom (
M,
N)
by A6;
verum
end;
dom ((LMULT (M,N)) | [: the carrier of R,(set_Hom (M,N)):]) = [: the carrier of R,(set_Hom (M,N)):]
by A1, RELAT_1:62, ZFMISC_1:96;
hence
(LMULT (M,N)) | [: the carrier of R,(set_Hom (M,N)):] is Function of [: the carrier of R,(set_Hom (M,N)):],(set_Hom (M,N))
by A2, FUNCT_2:3; verum