environ
vocabularies HIDDEN, NUMBERS, NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_1, XXREAL_0, CARD_1, ARYTM_1, ARYTM_3, TARSKI, RELAT_1, FUNCT_1, ORDINAL4, FUNCT_2, FUNCOP_1, ZFMISC_1, PARTFUN1, FINSEQ_2, PBOOLE, CARD_3, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, DOMAIN_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, FINSEQ_1, BINOP_1, PBOOLE, FUNCOP_1, CARD_3, XXREAL_0;
definitions TARSKI, FUNCT_1, FINSEQ_1, CARD_1, PBOOLE;
theorems TARSKI, ZFMISC_1, ENUMSET1, NAT_1, FUNCT_1, FUNCT_2, FUNCT_3, FINSEQ_1, FUNCOP_1, RELAT_1, RELSET_1, XBOOLE_1, XREAL_1, GRFUNC_1, XXREAL_0, ORDINAL1, CARD_1, SUBSET_1, CARD_3;
schemes FINSEQ_1, NAT_1, FRAENKEL, PBOOLE, FUNCT_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCOP_1, XREAL_0, NAT_1, FINSEQ_1, CARD_1, RELSET_1, CARD_3;
constructors HIDDEN, RELAT_2, PARTFUN1, BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, SQUARE_1, NAT_1, FINSEQ_1, RELSET_1, PBOOLE, CARD_3, SETFAM_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_1, FUNCOP_1, ORDINAL1;
expansions TARSKI, FUNCT_1, CARD_1, PBOOLE;
Lm1:
for x1, x2 being object holds rng <*x1,x2*> = {x1,x2}
Lm2:
for x1, x2, x3 being object holds rng <*x1,x2,x3*> = {x1,x2,x3}
Lm3:
for i being natural Number
for p, q being FinSequence
for F being Function st [:(rng p),(rng q):] c= dom F & i = min ((len p),(len q)) holds
dom (F .: (p,q)) = Seg i
Lm4:
for a being object
for p being FinSequence
for F being Function st [:{a},(rng p):] c= dom F holds
dom (F [;] (a,p)) = dom p
Lm5:
for a being object
for p being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F holds
dom (F [:] (p,a)) = dom p
theorem
for
D,
D9,
E being non
empty set for
d1,
d2 being
Element of
D for
d19,
d29 being
Element of
D9 for
F being
Function of
[:D,D9:],
E for
p being
FinSequence of
D for
q being
FinSequence of
D9 st
p = <*d1,d2*> &
q = <*d19,d29*> holds
F .: (
p,
q)
= <*(F . (d1,d19)),(F . (d2,d29))*>
theorem
for
D,
D9,
E being non
empty set for
d1,
d2,
d3 being
Element of
D for
d19,
d29,
d39 being
Element of
D9 for
F being
Function of
[:D,D9:],
E for
p being
FinSequence of
D for
q being
FinSequence of
D9 st
p = <*d1,d2,d3*> &
q = <*d19,d29,d39*> holds
F .: (
p,
q)
= <*(F . (d1,d19)),(F . (d2,d29)),(F . (d3,d39))*>
theorem
for
D,
D9,
E being non
empty set for
d being
Element of
D for
d19,
d29 being
Element of
D9 for
F being
Function of
[:D,D9:],
E for
p being
FinSequence of
D9 st
p = <*d19,d29*> holds
F [;] (
d,
p)
= <*(F . (d,d19)),(F . (d,d29))*>
theorem
for
D,
D9,
E being non
empty set for
d being
Element of
D for
d19,
d29,
d39 being
Element of
D9 for
F being
Function of
[:D,D9:],
E for
p being
FinSequence of
D9 st
p = <*d19,d29,d39*> holds
F [;] (
d,
p)
= <*(F . (d,d19)),(F . (d,d29)),(F . (d,d39))*>
theorem
for
D,
D9,
E being non
empty set for
d1,
d2 being
Element of
D for
d9 being
Element of
D9 for
F being
Function of
[:D,D9:],
E for
p being
FinSequence of
D st
p = <*d1,d2*> holds
F [:] (
p,
d9)
= <*(F . (d1,d9)),(F . (d2,d9))*>
theorem
for
D,
D9,
E being non
empty set for
d1,
d2,
d3 being
Element of
D for
d9 being
Element of
D9 for
F being
Function of
[:D,D9:],
E for
p being
FinSequence of
D st
p = <*d1,d2,d3*> holds
F [:] (
p,
d9)
= <*(F . (d1,d9)),(F . (d2,d9)),(F . (d3,d9))*>
Lm6:
for i being natural Number
for D being non empty set
for z being Tuple of i,D holds z in i -tuples_on D
Lm7:
for i being natural Number
for A being set
for x being object st x in i -tuples_on A holds
x is b1 -element FinSequence
::$CT