begin
Lm1:
for n being Nat
for f being real-valued b1 -element FinSequence holds f is Element of n -tuples_on REAL
definition
let n be
Nat;
set T =
TOP-REAL n;
set c = the
carrier of
(TOP-REAL n);
A1:
the
carrier of
[:(TOP-REAL n),(TOP-REAL n):] = [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]
by BORSUK_1:def 2;
existence
ex b1 being Function of [:(TOP-REAL n),(TOP-REAL n):],(TOP-REAL n) st
for x, y being Point of (TOP-REAL n) holds b1 . (x,y) = x (#) y
uniqueness
for b1, b2 being Function of [:(TOP-REAL n),(TOP-REAL n):],(TOP-REAL n) st ( for x, y being Point of (TOP-REAL n) holds b1 . (x,y) = x (#) y ) & ( for x, y being Point of (TOP-REAL n) holds b2 . (x,y) = x (#) y ) holds
b1 = b2
end;
begin