set f = trans_prod (F,a);
set g = (trans_prod (F,a)) | (sum F);
set G = F * a;
A2:
dom ((trans_prod (F,a)) | (sum F)) = [#] (sum F)
by FUNCT_2:def 1;
for y being object st y in rng ((trans_prod (F,a)) | (sum F)) holds
y in [#] (sum (F * a))
proof
let y be
object ;
( y in rng ((trans_prod (F,a)) | (sum F)) implies y in [#] (sum (F * a)) )
assume A3:
y in rng ((trans_prod (F,a)) | (sum F))
;
y in [#] (sum (F * a))
then consider x being
object such that A4:
x in dom ((trans_prod (F,a)) | (sum F))
and A5:
y = ((trans_prod (F,a)) | (sum F)) . x
by FUNCT_1:def 3;
[#] (sum F) c= [#] (product F)
by GROUP_2:def 5;
then reconsider x =
x as
Element of
(product F) by A4;
reconsider y =
y as
Element of
(product (F * a)) by A3;
A6:
dom a = I
by FUNCT_2:def 1;
y = (trans_prod (F,a)) . x
by A4, A5, FUNCT_1:49;
then A7:
y = x * a
by Def2;
then A8:
a .: (support (y,(F * a))) c= support (
x,
F)
by Th7;
support (
x,
F)
c= a .: (support (y,(F * a)))
by A1, A7, Th8;
then
(a ") .: (support (x,F)) = (a ") .: (a .: (support (y,(F * a))))
by A8, XBOOLE_0:def 10;
then
support (
y,
(F * a)) is
finite
by A1, A4, A6, FUNCT_1:107;
then
y in sum (F * a)
by GROUP_19:8;
hence
y in [#] (sum (F * a))
;
verum
end;
hence
(trans_prod (F,a)) | (sum F) is Function of (sum F),(sum (F * a))
by A2, FUNCT_2:2, TARSKI:def 3; verum