environ
vocabularies HIDDEN, RELAT_1, FUNCT_1, VALUED_0, TOPS_1, MEMBERED, XBOOLE_0, ARYTM_1, COMPLEX1, ARYTM_3, XCMPLX_0, FINSEQ_1, EUCLID, PRE_TOPC, ORDINAL2, TOPREALB, METRIC_1, TOPMETR, RCOMP_1, PCOMPS_1, FUNCT_3, FINSEQ_2, RLVECT_1, RVSUM_1, SQUARE_1, FUNCT_4, VALUED_2, ALGSTR_0, SUBSET_1, FUNCOP_1, PARTFUN1, CARD_3, FINSET_1, ZFMISC_1, TARSKI, CARD_1, TOPREALC, NAT_1, XXREAL_0, VALUED_1, NUMBERS, ORDINAL4, STRUCT_0, XXREAL_1, SUPINF_2, FUNCT_7, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, ORDINAL1, CARD_1, NUMBERS, VALUED_0, VALUED_1, XCMPLX_0, XREAL_0, XXREAL_0, FUNCT_3, MEMBERED, COMPLEX1, SQUARE_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, RCOMP_1, FUNCT_7, VALUED_2, STRUCT_0, RVSUM_1, PRE_TOPC, TOPS_1, METRIC_1, PCOMPS_1, TOPMETR, T_0TOPSP, BORSUK_1, ALGSTR_0, RLVECT_1, RLTOPSP1, EUCLID, WAYBEL18, TOPREAL9, TOPREALB;
definitions TARSKI, XBOOLE_0, LATTICE7, FUNCT_1, FUNCT_2, VALUED_0, VALUED_2, STRUCT_0, TOPMETR;
theorems FUNCT_1, PARTFUN1, FUNCT_2, VALUED_1, FUNCT_7, SEQ_2, VALUED_2, BORSUK_1, TOPREALB, TOPMETR, TOPREAL9, EUCLID, JGRAPH_2, JGRAPH_6, GOBOARD6, TOPS_1, METRIC_1, JGRAPH_1, TOPRNS_1, XXREAL_0, XREAL_1, XBOOLE_0, RCOMP_1, JORDAN2B, FINSEQ_2, XREAL_0, FINSEQ_1, NAT_1, FUNCOP_1, PRE_TOPC, SQUARE_1, TOPREAL6, RVSUM_1, COMPLEX1, XXREAL_1, XCMPLX_1, ORDINAL1, TSP_1, RLVECT_1, TOPS_3, YELLOW12, TOPGEN_5, YELLOW17, ZFMISC_1, REAL_NS1, WAYBEL18, BINOP_1, JGRAPH_4, ABSVALUE, CARD_1, STRUCT_0, PRVECT_2, TOPREAL7, EUCLID_9, TOPS_4, NAT_D;
schemes FUNCT_2, BINOP_1, FINSEQ_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, VALUED_0, VALUED_1, MEMBERED, XCMPLX_0, XREAL_0, VALUED_2, PRE_TOPC, STRUCT_0, EUCLID, MONOID_0, TOPREALB, XXREAL_0, NAT_1, TOPMETR, FUNCT_2, RVSUM_1, TOPREAL9, SQUARE_1, RCOMP_1, TOPS_1, FUNCT_7, NUMBERS, RLVECT_1, FINSEQ_1, FUNCOP_1, WAYBEL18, BORSUK_1, PRE_POLY, JORDAN2B, FINSEQ_2, PARTFUN3, EUCLID_9, CARD_1, FINSET_1, RELSET_1;
constructors HIDDEN, MONOID_0, FUNCT_7, FINSEQOP, VALUED_2, TOPREAL9, TOPREALB, TOPS_1, COMPLEX1, T_0TOPSP, SQUARE_1, FUNCT_4, FUNCSDOM, CONVEX1, WAYBEL18, BINOP_2, EUCLID_9, PARTFUN3, REAL_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
equalities FINSEQ_1, RLVECT_1, XCMPLX_0, SQUARE_1, BINOP_1, FUNCOP_1, VALUED_1, FINSEQ_2, VALUED_2, STRUCT_0, METRIC_1, PCOMPS_1, TOPMETR, CONVEX1, RLTOPSP1, EUCLID, TOPREALB, RVSUM_1, ORDINAL1;
expansions XBOOLE_0, FUNCT_1, STRUCT_0, TOPMETR;
Lm1:
for n being Nat
for f being b1 -element real-valued 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;