begin
Lm1:
for x1, x2 being set holds rng <*x1,x2*> = {x1,x2}
Lm2:
for x1, x2, x3 being set holds rng <*x1,x2,x3*> = {x1,x2,x3}
Lm3:
for i being Nat
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 set
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 set
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 Nat
for D being non empty set
for z being Tuple of i,D holds z in i -tuples_on D
Lm7:
for i being Nat
for x, A being set st x in i -tuples_on A holds
x is b1 -element FinSequence
theorem
for
i being
Nat for
D being non
empty set for
z1,
z2 being
Tuple of
i,
D st ( for
j being
Nat st
j in Seg i holds
z1 . j = z2 . j ) holds
z1 = z2
begin