environ
vocabularies HIDDEN, SUBSET_1, NUMBERS, FINSEQ_1, FINSEQ_2, ARYTM_3, NAT_1, XXREAL_0, FUNCT_1, RELAT_1, TARSKI, BINOP_2, FUNCOP_1, ARYTM_1, XCMPLX_0, CARD_1, COMPLEX1, RVSUM_1, REAL_1, ZFMISC_1, VALUED_0;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, PARTFUN1, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQOP, VALUED_0, VALUED_1, SEQ_4, COMPLEX1, RVSUM_1, FINSEQ_2, BINOP_2, MATRIX_5, XXREAL_0, COMSEQ_2;
definitions TARSKI;
theorems FUNCT_1, FUNCT_2, FINSEQ_1, FUNCOP_1, FINSEQ_2, FINSEQOP, RELAT_1, BINOP_2, COMPLEX1, XCMPLX_0, FINSEQ_3, RVSUM_1, ORDINAL1, VALUED_0, VALUED_1, SEQ_4, CARD_1, XREAL_0, COMSEQ_2;
schemes ;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, BINOP_2, MEMBERED, FINSEQ_2, VALUED_0, VALUED_1, XREAL_0;
constructors HIDDEN, SETWISEO, REAL_1, BINOP_2, FINSEQOP, SEQ_4, MATRIX_5, BINOP_1, RVSUM_1, RELSET_1, COMSEQ_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities VALUED_1, ORDINAL1;
expansions FINSEQ_1;
Lm1:
for x being FinSequence of COMPLEX
for c being Element of COMPLEX holds c * x = (multcomplex [;] (c,(id COMPLEX))) * x
Lm2:
for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
theorem Th38:
for
C being
Function of
[:COMPLEX,COMPLEX:],
COMPLEX for
G being
Function of
[:REAL,REAL:],
REAL for
x1,
y1 being
FinSequence of
COMPLEX for
x2,
y2 being
FinSequence of
REAL st
x1 = x2 &
y1 = y2 &
len x1 = len y2 & ( for
i being
Element of
NAT st
i in dom x1 holds
C . (
(x1 . i),
(y1 . i))
= G . (
(x2 . i),
(y2 . i)) ) holds
C .: (
x1,
y1)
= G .: (
x2,
y2)
Lm3:
for x being FinSequence of COMPLEX holds - (0c (len x)) = 0c (len x)