begin
Lm1:
for n being Nat ex ADD being BinOp of (REAL n) st
( ( for a, b being Element of REAL n holds ADD . (a,b) = a + b ) & ADD is commutative & ADD is associative )
Lm2:
for n being Nat holds REAL-NS n is RealBanachSpace
begin
definition
let n be
Nat;
existence
ex b1 being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds b1 . (x,y) = Sum (mlt (x,y))
uniqueness
for b1, b2 being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b1 . (x,y) = Sum (mlt (x,y)) ) & ( for x, y being Element of REAL n holds b2 . (x,y) = Sum (mlt (x,y)) ) holds
b1 = b2
end;