let n be non empty Nat; :: thesis: 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; :: thesis: (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)

proof

let i be Element of Seg n; :: thesis: h . i = (x0 . i) + (y0 . i)
A2: (product ( the addF of F_Real,n)) . (x0,y0) = addreal .: (x0,y0) by PRVECT_1:def 1;
dom h = Seg n by FUNCT_2:def 1;
hence h . i = addreal . ((x0 . i),(y0 . i)) by FUNCOP_1:22, A2
.= (x0 . i) + (y0 . i) by BINOP_2:def 9 ;
:: thesis: verum

end;

hence (RealFuncAdd (Seg n)) . (x,y) = (product ( the addF of F_Real,n)) . (x,y) by FUNCSDOM:1; :: thesis: verum

end;

hence RealFuncAdd (Seg n) = product ( the addF of F_Real,n) by BINOP_1:2, A1; :: thesis: verum