let n be non empty Nat; :: thesis: RealFuncExtMult (Seg n) = n -Mult_over F_Real
set OP1 = RealFuncExtMult (Seg n);
set OP2 = n -Mult_over F_Real;
A1: Funcs ((Seg n),REAL) = REAL n by FINSEQ_2:93;
for x being Element of REAL
for y being Element of REAL n holds (RealFuncExtMult (Seg n)) . (x,y) = (n -Mult_over F_Real) . (x,y)

proof

let x be Element of REAL ; :: thesis: for y being Element of REAL n holds (RealFuncExtMult (Seg n)) . (x,y) = (n -Mult_over F_Real) . (x,y)
let y be Element of REAL n; :: thesis: (RealFuncExtMult (Seg n)) . (x,y) = (n -Mult_over F_Real) . (x,y)
reconsider y0 = y as Element of Funcs ((Seg n),REAL) by FINSEQ_2:93;
[x,y] in [:REAL,(REAL n):] by ZFMISC_1:87;
then (n -Mult_over F_Real) . (x,y) in REAL n by FUNCT_2:5;
then reconsider h = (n -Mult_over F_Real) . (x,y0) as Element of Funcs ((Seg n),REAL) by FINSEQ_2:93;
for i being Element of Seg n holds h . i = x * (y0 . i)

proof

let i be Element of Seg n; :: thesis: h . i = x * (y0 . i)
A2: (n -Mult_over F_Real) . [x,y0] = (n -Mult_over F_Real) . (x,y0)
.= multreal [;] (x,y0) by PRVECT_1:def 4 ;
dom h = Seg n by FUNCT_2:def 1;
hence h . i = multreal . (x,(y0 . i)) by FUNCOP_1:32, A2
.= x * (y0 . i) by BINOP_2:def 11 ;
:: thesis: verum

end;

hence (RealFuncExtMult (Seg n)) . (x,y) = (n -Mult_over F_Real) . (x,y) by FUNCSDOM:4; :: thesis: verum

end;

hence RealFuncExtMult (Seg n) = n -Mult_over F_Real by BINOP_1:2, A1; :: thesis: verum