let n be non empty Nat; RealFuncAdd (Seg n) = product ( the addF of F_Real,n)
set OP1 = RealFuncAdd (Seg n);
set OP2 = product ( the addF of F_Real,n);
A1:
Funcs ((Seg n),REAL) = REAL n
by FINSEQ_2:93;
for x, y being Element of REAL n holds (RealFuncAdd (Seg n)) . (x,y) = (product ( the addF of F_Real,n)) . (x,y)
proof
let x,
y be
Element of
REAL n;
(RealFuncAdd (Seg n)) . (x,y) = (product ( the addF of F_Real,n)) . (x,y)
reconsider x0 =
x,
y0 =
y as
Element of
Funcs (
(Seg n),
REAL)
by FINSEQ_2:93;
[x,y] in [:(REAL n),(REAL n):]
by ZFMISC_1:87;
then
(product ( the addF of F_Real,n)) . (
x,
y)
in REAL n
by FUNCT_2:5;
then reconsider h =
(product ( the addF of F_Real,n)) . (
x0,
y0) as
Element of
Funcs (
(Seg n),
REAL)
by FINSEQ_2:93;
for
i being
Element of
Seg n holds
h . i = (x0 . i) + (y0 . i)
hence
(RealFuncAdd (Seg n)) . (
x,
y)
= (product ( the addF of F_Real,n)) . (
x,
y)
by FUNCSDOM:1;
verum
end;
hence
RealFuncAdd (Seg n) = product ( the addF of F_Real,n)
by BINOP_1:2, A1; verum