:: FINSEQ_2 semantic presentation
begin
theorem :: FINSEQ_2:1
for i, j being Nat holds
( min (i,j) is Element of NAT & max (i,j) is Element of NAT ) by ORDINAL1:def_12;
theorem Th2: :: FINSEQ_2:2
for l, i, j being Nat st l = min (i,j) holds
(Seg i) /\ (Seg j) = Seg l
proof
let l, i, j be Nat; ::_thesis: ( l = min (i,j) implies (Seg i) /\ (Seg j) = Seg l )
( i <= j or j <= i ) ;
then ( ( i <= j & (Seg i) /\ (Seg j) = Seg i ) or ( j <= i & (Seg i) /\ (Seg j) = Seg j ) ) by FINSEQ_1:7;
hence ( l = min (i,j) implies (Seg i) /\ (Seg j) = Seg l ) by XXREAL_0:def_9; ::_thesis: verum
end;
theorem Th3: :: FINSEQ_2:3
for i, j being Nat st i <= j holds
max (0,(i - j)) = 0
proof
let i, j be Nat; ::_thesis: ( i <= j implies max (0,(i - j)) = 0 )
assume i <= j ; ::_thesis: max (0,(i - j)) = 0
then i - i <= j - i by XREAL_1:9;
then - (j - i) <= - 0 ;
hence max (0,(i - j)) = 0 by XXREAL_0:def_10; ::_thesis: verum
end;
theorem Th4: :: FINSEQ_2:4
for j, i being Nat st j <= i holds
max (0,(i - j)) = i - j
proof
let j, i be Nat; ::_thesis: ( j <= i implies max (0,(i - j)) = i - j )
assume j <= i ; ::_thesis: max (0,(i - j)) = i - j
then j - j <= i - j by XREAL_1:9;
hence max (0,(i - j)) = i - j by XXREAL_0:def_10; ::_thesis: verum
end;
theorem :: FINSEQ_2:5
for i, j being Nat holds max (0,(i - j)) is Element of NAT
proof
let i, j be Nat; ::_thesis: max (0,(i - j)) is Element of NAT
percases ( i <= j or j <= i ) ;
suppose i <= j ; ::_thesis: max (0,(i - j)) is Element of NAT
hence max (0,(i - j)) is Element of NAT by Th3; ::_thesis: verum
end;
supposeA1: j <= i ; ::_thesis: max (0,(i - j)) is Element of NAT
then i - j is Element of NAT by NAT_1:21;
hence max (0,(i - j)) is Element of NAT by A1, Th4; ::_thesis: verum
end;
end;
end;
theorem :: FINSEQ_2:6
for i being Nat holds
( min (0,i) = 0 & min (i,0) = 0 & max (0,i) = i & max (i,0) = i ) by XXREAL_0:def_9, XXREAL_0:def_10;
theorem :: FINSEQ_2:7
for i, l being Nat holds
( not i in Seg (l + 1) or i in Seg l or i = l + 1 )
proof
let i, l be Nat; ::_thesis: ( not i in Seg (l + 1) or i in Seg l or i = l + 1 )
assume A1: i in Seg (l + 1) ; ::_thesis: ( i in Seg l or i = l + 1 )
then i <= l + 1 by FINSEQ_1:1;
then A2: ( ( 1 <= i & i <= l ) or i = l + 1 ) by A1, FINSEQ_1:1, NAT_1:8;
i is Element of NAT by ORDINAL1:def_12;
hence ( i in Seg l or i = l + 1 ) by A2; ::_thesis: verum
end;
theorem :: FINSEQ_2:8
for i, l, j being Nat st i in Seg l holds
i in Seg (l + j)
proof
let i, l, j be Nat; ::_thesis: ( i in Seg l implies i in Seg (l + j) )
l <= l + j by NAT_1:11;
then Seg l c= Seg (l + j) by FINSEQ_1:5;
hence ( i in Seg l implies i in Seg (l + j) ) ; ::_thesis: verum
end;
theorem :: FINSEQ_2:9
for p, q being FinSequence st len p = len q & ( for j being Nat st j in dom p holds
p . j = q . j ) holds
p = q
proof
let p, q be FinSequence; ::_thesis: ( len p = len q & ( for j being Nat st j in dom p holds
p . j = q . j ) implies p = q )
assume that
A1: len p = len q and
A2: for j being Nat st j in dom p holds
p . j = q . j ; ::_thesis: p = q
( dom p = Seg (len p) & dom q = Seg (len p) ) by A1, FINSEQ_1:def_3;
hence p = q by A2, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th10: :: FINSEQ_2:10
for b being set
for p being FinSequence st b in rng p holds
ex i being Nat st
( i in dom p & p . i = b )
proof
let b be set ; ::_thesis: for p being FinSequence st b in rng p holds
ex i being Nat st
( i in dom p & p . i = b )
let p be FinSequence; ::_thesis: ( b in rng p implies ex i being Nat st
( i in dom p & p . i = b ) )
assume b in rng p ; ::_thesis: ex i being Nat st
( i in dom p & p . i = b )
then ex a being set st
( a in dom p & b = p . a ) by FUNCT_1:def_3;
hence ex i being Nat st
( i in dom p & p . i = b ) ; ::_thesis: verum
end;
theorem Th11: :: FINSEQ_2:11
for i being Nat
for D being set
for p being FinSequence of D st i in dom p holds
p . i in D
proof
let i be Nat; ::_thesis: for D being set
for p being FinSequence of D st i in dom p holds
p . i in D
let D be set ; ::_thesis: for p being FinSequence of D st i in dom p holds
p . i in D
let p be FinSequence of D; ::_thesis: ( i in dom p implies p . i in D )
assume i in dom p ; ::_thesis: p . i in D
then A1: p . i in rng p by FUNCT_1:def_3;
rng p c= D by FINSEQ_1:def_4;
hence p . i in D by A1; ::_thesis: verum
end;
theorem Th12: :: FINSEQ_2:12
for p being FinSequence
for D being set st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is FinSequence of D
proof
let p be FinSequence; ::_thesis: for D being set st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is FinSequence of D
let D be set ; ::_thesis: ( ( for i being Nat st i in dom p holds
p . i in D ) implies p is FinSequence of D )
assume A1: for i being Nat st i in dom p holds
p . i in D ; ::_thesis: p is FinSequence of D
let b be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not b in rng p or b in D )
assume b in rng p ; ::_thesis: b in D
then ex i being Nat st
( i in dom p & p . i = b ) by Th10;
hence b in D by A1; ::_thesis: verum
end;
Lm1: for x1, x2 being set holds rng <*x1,x2*> = {x1,x2}
proof
let x1, x2 be set ; ::_thesis: rng <*x1,x2*> = {x1,x2}
thus rng <*x1,x2*> = (rng <*x1*>) \/ (rng <*x2*>) by FINSEQ_1:31
.= (rng <*x1*>) \/ {x2} by FINSEQ_1:38
.= {x1} \/ {x2} by FINSEQ_1:39
.= {x1,x2} by ENUMSET1:1 ; ::_thesis: verum
end;
theorem Th13: :: FINSEQ_2:13
for D being non empty set
for d1, d2 being Element of D holds <*d1,d2*> is FinSequence of D
proof
let D be non empty set ; ::_thesis: for d1, d2 being Element of D holds <*d1,d2*> is FinSequence of D
let d1, d2 be Element of D; ::_thesis: <*d1,d2*> is FinSequence of D
rng <*d1,d2*> = {d1,d2} by Lm1;
hence <*d1,d2*> is FinSequence of D by FINSEQ_1:def_4; ::_thesis: verum
end;
Lm2: for x1, x2, x3 being set holds rng <*x1,x2,x3*> = {x1,x2,x3}
proof
let x1, x2, x3 be set ; ::_thesis: rng <*x1,x2,x3*> = {x1,x2,x3}
thus rng <*x1,x2,x3*> = rng (<*x1*> ^ <*x2,x3*>) by FINSEQ_1:43
.= (rng <*x1*>) \/ (rng <*x2,x3*>) by FINSEQ_1:31
.= {x1} \/ (rng <*x2,x3*>) by FINSEQ_1:38
.= {x1} \/ {x2,x3} by Lm1
.= {x1,x2,x3} by ENUMSET1:2 ; ::_thesis: verum
end;
theorem Th14: :: FINSEQ_2:14
for D being non empty set
for d1, d2, d3 being Element of D holds <*d1,d2,d3*> is FinSequence of D
proof
let D be non empty set ; ::_thesis: for d1, d2, d3 being Element of D holds <*d1,d2,d3*> is FinSequence of D
let d1, d2, d3 be Element of D; ::_thesis: <*d1,d2,d3*> is FinSequence of D
rng <*d1,d2,d3*> = {d1,d2,d3} by Lm2;
hence <*d1,d2,d3*> is FinSequence of D by FINSEQ_1:def_4; ::_thesis: verum
end;
theorem Th15: :: FINSEQ_2:15
for i being Nat
for p, q being FinSequence st i in dom p holds
i in dom (p ^ q)
proof
let i be Nat; ::_thesis: for p, q being FinSequence st i in dom p holds
i in dom (p ^ q)
let p, q be FinSequence; ::_thesis: ( i in dom p implies i in dom (p ^ q) )
A1: dom p c= dom (p ^ q) by FINSEQ_1:26;
assume i in dom p ; ::_thesis: i in dom (p ^ q)
hence i in dom (p ^ q) by A1; ::_thesis: verum
end;
theorem Th16: :: FINSEQ_2:16
for a being set
for p being FinSequence holds len (p ^ <*a*>) = (len p) + 1
proof
let a be set ; ::_thesis: for p being FinSequence holds len (p ^ <*a*>) = (len p) + 1
let p be FinSequence; ::_thesis: len (p ^ <*a*>) = (len p) + 1
len (p ^ <*a*>) = (len p) + (len <*a*>) by FINSEQ_1:22;
hence len (p ^ <*a*>) = (len p) + 1 by FINSEQ_1:39; ::_thesis: verum
end;
theorem :: FINSEQ_2:17
for a, b being set
for p, q being FinSequence st p ^ <*a*> = q ^ <*b*> holds
( p = q & a = b )
proof
let a, b be set ; ::_thesis: for p, q being FinSequence st p ^ <*a*> = q ^ <*b*> holds
( p = q & a = b )
let p, q be FinSequence; ::_thesis: ( p ^ <*a*> = q ^ <*b*> implies ( p = q & a = b ) )
assume A1: p ^ <*a*> = q ^ <*b*> ; ::_thesis: ( p = q & a = b )
A2: ( (p ^ <*a*>) . ((len p) + 1) = a & (q ^ <*b*>) . ((len q) + 1) = b ) by FINSEQ_1:42;
( len (p ^ <*a*>) = (len p) + 1 & len (q ^ <*b*>) = (len q) + 1 ) by Th16;
hence ( p = q & a = b ) by A1, A2, FINSEQ_1:33; ::_thesis: verum
end;
theorem :: FINSEQ_2:18
for i being Nat
for p being FinSequence st len p = i + 1 holds
ex q being FinSequence ex a being set st p = q ^ <*a*> by CARD_1:27, FINSEQ_1:46;
theorem Th19: :: FINSEQ_2:19
for A being set
for p being FinSequence of A st len p <> 0 holds
ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*>
proof
let A be set ; ::_thesis: for p being FinSequence of A st len p <> 0 holds
ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*>
let p be FinSequence of A; ::_thesis: ( len p <> 0 implies ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*> )
assume A1: len p <> 0 ; ::_thesis: ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*>
then p <> {} ;
then consider q being FinSequence, d being set such that
A2: p = q ^ <*d*> by FINSEQ_1:46;
for i being Nat st i in dom q holds
q . i in A
proof
let i be Nat; ::_thesis: ( i in dom q implies q . i in A )
assume i in dom q ; ::_thesis: q . i in A
then ( p . i = q . i & i in dom p ) by A2, Th15, FINSEQ_1:def_7;
hence q . i in A by Th11; ::_thesis: verum
end;
then A3: q is FinSequence of A by Th12;
len p in Seg (len p) by A1, FINSEQ_1:3;
then A4: len p in dom p by FINSEQ_1:def_3;
len p = (len q) + 1 by A2, Th16;
then p . (len p) = d by A2, FINSEQ_1:42;
then d is Element of A by A4, Th11;
hence ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*> by A2, A3; ::_thesis: verum
end;
theorem Th20: :: FINSEQ_2:20
for i being Nat
for q, p being FinSequence st q = p | (Seg i) & len p <= i holds
p = q
proof
let i be Nat; ::_thesis: for q, p being FinSequence st q = p | (Seg i) & len p <= i holds
p = q
let q, p be FinSequence; ::_thesis: ( q = p | (Seg i) & len p <= i implies p = q )
assume A1: q = p | (Seg i) ; ::_thesis: ( not len p <= i or p = q )
assume len p <= i ; ::_thesis: p = q
then Seg (len p) c= Seg i by FINSEQ_1:5;
then dom p c= Seg i by FINSEQ_1:def_3;
hence p = q by A1, RELAT_1:68; ::_thesis: verum
end;
theorem :: FINSEQ_2:21
for i being Nat
for q, p being FinSequence st q = p | (Seg i) holds
len q = min (i,(len p))
proof
let i be Nat; ::_thesis: for q, p being FinSequence st q = p | (Seg i) holds
len q = min (i,(len p))
let q, p be FinSequence; ::_thesis: ( q = p | (Seg i) implies len q = min (i,(len p)) )
assume A1: q = p | (Seg i) ; ::_thesis: len q = min (i,(len p))
now__::_thesis:_(_(_i_<=_len_p_&_len_q_=_i_)_or_(_not_i_<=_len_p_&_len_q_=_len_p_)_)
percases ( i <= len p or not i <= len p ) ;
case i <= len p ; ::_thesis: len q = i
hence len q = i by A1, FINSEQ_1:17; ::_thesis: verum
end;
case not i <= len p ; ::_thesis: len q = len p
hence len q = len p by A1, Th20; ::_thesis: verum
end;
end;
end;
hence len q = min (i,(len p)) by XXREAL_0:def_9; ::_thesis: verum
end;
theorem Th22: :: FINSEQ_2:22
for i, j being Nat
for r being FinSequence st len r = i + j holds
ex p, q being FinSequence st
( len p = i & len q = j & r = p ^ q )
proof
let i, j be Nat; ::_thesis: for r being FinSequence st len r = i + j holds
ex p, q being FinSequence st
( len p = i & len q = j & r = p ^ q )
let r be FinSequence; ::_thesis: ( len r = i + j implies ex p, q being FinSequence st
( len p = i & len q = j & r = p ^ q ) )
assume A1: len r = i + j ; ::_thesis: ex p, q being FinSequence st
( len p = i & len q = j & r = p ^ q )
reconsider z = i as Element of NAT by ORDINAL1:def_12;
reconsider p = r | (Seg z) as FinSequence by FINSEQ_1:15;
consider q being FinSequence such that
A2: r = p ^ q by FINSEQ_1:80;
take p ; ::_thesis: ex q being FinSequence st
( len p = i & len q = j & r = p ^ q )
take q ; ::_thesis: ( len p = i & len q = j & r = p ^ q )
i <= len r by A1, NAT_1:11;
hence len p = i by FINSEQ_1:17; ::_thesis: ( len q = j & r = p ^ q )
then len (p ^ q) = i + (len q) by FINSEQ_1:22;
hence len q = j by A1, A2; ::_thesis: r = p ^ q
thus r = p ^ q by A2; ::_thesis: verum
end;
theorem Th23: :: FINSEQ_2:23
for i, j being Nat
for D being non empty set
for r being FinSequence of D st len r = i + j holds
ex p, q being FinSequence of D st
( len p = i & len q = j & r = p ^ q )
proof
let i, j be Nat; ::_thesis: for D being non empty set
for r being FinSequence of D st len r = i + j holds
ex p, q being FinSequence of D st
( len p = i & len q = j & r = p ^ q )
let D be non empty set ; ::_thesis: for r being FinSequence of D st len r = i + j holds
ex p, q being FinSequence of D st
( len p = i & len q = j & r = p ^ q )
let r be FinSequence of D; ::_thesis: ( len r = i + j implies ex p, q being FinSequence of D st
( len p = i & len q = j & r = p ^ q ) )
assume len r = i + j ; ::_thesis: ex p, q being FinSequence of D st
( len p = i & len q = j & r = p ^ q )
then consider p, q being FinSequence such that
A1: ( len p = i & len q = j ) and
A2: r = p ^ q by Th22;
( p is FinSequence of D & q is FinSequence of D ) by A2, FINSEQ_1:36;
hence ex p, q being FinSequence of D st
( len p = i & len q = j & r = p ^ q ) by A1, A2; ::_thesis: verum
end;
scheme :: FINSEQ_2:sch 1
SeqLambdaD{ F1() -> Nat, F2() -> non empty set , F3( set ) -> Element of F2() } :
ex z being FinSequence of F2() st
( len z = F1() & ( for j being Nat st j in dom z holds
z . j = F3(j) ) )
proof
consider z being FinSequence such that
A1: len z = F1() and
A2: for i being Nat st i in dom z holds
z . i = F3(i) from FINSEQ_1:sch_2();
A3: Seg F1() = dom z by A1, FINSEQ_1:def_3;
for j being Nat st j in Seg F1() holds
z . j in F2()
proof
let j be Nat; ::_thesis: ( j in Seg F1() implies z . j in F2() )
assume j in Seg F1() ; ::_thesis: z . j in F2()
then z . j = F3(j) by A2, A3;
hence z . j in F2() ; ::_thesis: verum
end;
then reconsider z = z as FinSequence of F2() by A3, Th12;
take z ; ::_thesis: ( len z = F1() & ( for j being Nat st j in dom z holds
z . j = F3(j) ) )
thus len z = F1() by A1; ::_thesis: for j being Nat st j in dom z holds
z . j = F3(j)
let j be Nat; ::_thesis: ( j in dom z implies z . j = F3(j) )
thus ( j in dom z implies z . j = F3(j) ) by A2; ::_thesis: verum
end;
scheme :: FINSEQ_2:sch 2
IndSeqD{ F1() -> set , P1[ set ] } :
for p being FinSequence of F1() holds P1[p]
provided
A1: P1[ <*> F1()] and
A2: for p being FinSequence of F1()
for x being Element of F1() st P1[p] holds
P1[p ^ <*x*>]
proof
defpred S1[ set ] means for p being FinSequence of F1() st len p = $1 holds
P1[p];
A3: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A4: for p being FinSequence of F1() st len p = i holds
P1[p] ; ::_thesis: S1[i + 1]
let p be FinSequence of F1(); ::_thesis: ( len p = i + 1 implies P1[p] )
assume A5: len p = i + 1 ; ::_thesis: P1[p]
then consider q being FinSequence of F1(), x being Element of F1() such that
A6: p = q ^ <*x*> by Th19;
len p = (len q) + 1 by A6, Th16;
hence P1[p] by A2, A4, A5, A6; ::_thesis: verum
end;
let p be FinSequence of F1(); ::_thesis: P1[p]
A7: len p = len p ;
A8: S1[ 0 ]
proof
let p be FinSequence of F1(); ::_thesis: ( len p = 0 implies P1[p] )
assume len p = 0 ; ::_thesis: P1[p]
then p = <*> F1() ;
hence P1[p] by A1; ::_thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch_2(A8, A3);
hence P1[p] by A7; ::_thesis: verum
end;
theorem Th24: :: FINSEQ_2:24
for D being set
for D1 being Subset of D
for p being FinSequence of D1 holds p is FinSequence of D
proof
let D be set ; ::_thesis: for D1 being Subset of D
for p being FinSequence of D1 holds p is FinSequence of D
let D1 be Subset of D; ::_thesis: for p being FinSequence of D1 holds p is FinSequence of D
let p be FinSequence of D1; ::_thesis: p is FinSequence of D
rng p c= D1 by FINSEQ_1:def_4;
hence rng p c= D by XBOOLE_1:1; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
theorem Th25: :: FINSEQ_2:25
for i being Nat
for D being non empty set
for f being Function of (Seg i),D holds f is FinSequence of D
proof
let i be Nat; ::_thesis: for D being non empty set
for f being Function of (Seg i),D holds f is FinSequence of D
let D be non empty set ; ::_thesis: for f being Function of (Seg i),D holds f is FinSequence of D
let f be Function of (Seg i),D; ::_thesis: f is FinSequence of D
reconsider i = i as Element of NAT by ORDINAL1:def_12;
dom f = Seg i by FUNCT_2:def_1;
then A1: f is FinSequence by FINSEQ_1:def_2;
rng f c= D by RELAT_1:def_19;
hence f is FinSequence of D by A1, FINSEQ_1:def_4; ::_thesis: verum
end;
theorem :: FINSEQ_2:26
for D being non empty set
for p being FinSequence of D holds p is Function of (dom p),D
proof
let D be non empty set ; ::_thesis: for p being FinSequence of D holds p is Function of (dom p),D
let p be FinSequence of D; ::_thesis: p is Function of (dom p),D
rng p c= D by FINSEQ_1:def_4;
hence p is Function of (dom p),D by FUNCT_2:2; ::_thesis: verum
end;
theorem :: FINSEQ_2:27
for i being Nat
for D being non empty set
for f being Function of NAT,D holds f | (Seg i) is FinSequence of D
proof
let i be Nat; ::_thesis: for D being non empty set
for f being Function of NAT,D holds f | (Seg i) is FinSequence of D
let D be non empty set ; ::_thesis: for f being Function of NAT,D holds f | (Seg i) is FinSequence of D
let f be Function of NAT,D; ::_thesis: f | (Seg i) is FinSequence of D
f | (Seg i) is Function of (Seg i),D by FUNCT_2:32;
hence f | (Seg i) is FinSequence of D by Th25; ::_thesis: verum
end;
theorem :: FINSEQ_2:28
for i being Nat
for D being non empty set
for q being FinSequence
for f being Function of NAT,D st q = f | (Seg i) holds
len q = i
proof
let i be Nat; ::_thesis: for D being non empty set
for q being FinSequence
for f being Function of NAT,D st q = f | (Seg i) holds
len q = i
let D be non empty set ; ::_thesis: for q being FinSequence
for f being Function of NAT,D st q = f | (Seg i) holds
len q = i
let q be FinSequence; ::_thesis: for f being Function of NAT,D st q = f | (Seg i) holds
len q = i
let f be Function of NAT,D; ::_thesis: ( q = f | (Seg i) implies len q = i )
reconsider i = i as Element of NAT by ORDINAL1:def_12;
f | (Seg i) is Function of (Seg i),D by FUNCT_2:32;
then dom (f | (Seg i)) = Seg i by FUNCT_2:def_1;
hence ( q = f | (Seg i) implies len q = i ) by FINSEQ_1:def_3; ::_thesis: verum
end;
theorem Th29: :: FINSEQ_2:29
for p, q being FinSequence
for f being Function st rng p c= dom f & q = f * p holds
len q = len p
proof
let p, q be FinSequence; ::_thesis: for f being Function st rng p c= dom f & q = f * p holds
len q = len p
let f be Function; ::_thesis: ( rng p c= dom f & q = f * p implies len q = len p )
assume rng p c= dom f ; ::_thesis: ( not q = f * p or len q = len p )
then dom (f * p) = dom p by RELAT_1:27;
then dom (f * p) = Seg (len p) by FINSEQ_1:def_3;
hence ( not q = f * p or len q = len p ) by FINSEQ_1:def_3; ::_thesis: verum
end;
theorem Th30: :: FINSEQ_2:30
for i being Nat
for D being non empty set st D = Seg i holds
for p being FinSequence
for q being FinSequence of D st i <= len p holds
p * q is FinSequence
proof
let i be Nat; ::_thesis: for D being non empty set st D = Seg i holds
for p being FinSequence
for q being FinSequence of D st i <= len p holds
p * q is FinSequence
let D be non empty set ; ::_thesis: ( D = Seg i implies for p being FinSequence
for q being FinSequence of D st i <= len p holds
p * q is FinSequence )
assume A1: D = Seg i ; ::_thesis: for p being FinSequence
for q being FinSequence of D st i <= len p holds
p * q is FinSequence
let p be FinSequence; ::_thesis: for q being FinSequence of D st i <= len p holds
p * q is FinSequence
let q be FinSequence of D; ::_thesis: ( i <= len p implies p * q is FinSequence )
assume i <= len p ; ::_thesis: p * q is FinSequence
then Seg i c= Seg (len p) by FINSEQ_1:5;
then A2: Seg i c= dom p by FINSEQ_1:def_3;
rng q c= Seg i by A1, FINSEQ_1:def_4;
then dom (p * q) = dom q by A2, RELAT_1:27, XBOOLE_1:1;
then dom (p * q) = Seg (len q) by FINSEQ_1:def_3;
hence p * q is FinSequence by FINSEQ_1:def_2; ::_thesis: verum
end;
theorem :: FINSEQ_2:31
for i being Nat
for D, D9 being non empty set st D = Seg i holds
for p being FinSequence of D9
for q being FinSequence of D st i <= len p holds
p * q is FinSequence of D9
proof
let i be Nat; ::_thesis: for D, D9 being non empty set st D = Seg i holds
for p being FinSequence of D9
for q being FinSequence of D st i <= len p holds
p * q is FinSequence of D9
let D, D9 be non empty set ; ::_thesis: ( D = Seg i implies for p being FinSequence of D9
for q being FinSequence of D st i <= len p holds
p * q is FinSequence of D9 )
assume A1: D = Seg i ; ::_thesis: for p being FinSequence of D9
for q being FinSequence of D st i <= len p holds
p * q is FinSequence of D9
let p be FinSequence of D9; ::_thesis: for q being FinSequence of D st i <= len p holds
p * q is FinSequence of D9
let q be FinSequence of D; ::_thesis: ( i <= len p implies p * q is FinSequence of D9 )
assume i <= len p ; ::_thesis: p * q is FinSequence of D9
then reconsider pq = p * q as FinSequence by A1, Th30;
( rng pq c= rng p & rng p c= D9 ) by FINSEQ_1:def_4, RELAT_1:26;
then rng pq c= D9 by XBOOLE_1:1;
hence p * q is FinSequence of D9 by FINSEQ_1:def_4; ::_thesis: verum
end;
theorem Th32: :: FINSEQ_2:32
for A, D being set
for p being FinSequence of A
for f being Function of A,D holds f * p is FinSequence of D
proof
let A, D be set ; ::_thesis: for p being FinSequence of A
for f being Function of A,D holds f * p is FinSequence of D
let p be FinSequence of A; ::_thesis: for f being Function of A,D holds f * p is FinSequence of D
let f be Function of A,D; ::_thesis: f * p is FinSequence of D
percases ( D = {} or D <> {} ) ;
suppose D = {} ; ::_thesis: f * p is FinSequence of D
then f * p = <*> D ;
hence f * p is FinSequence of D ; ::_thesis: verum
end;
supposeA1: D <> {} ; ::_thesis: f * p is FinSequence of D
A2: rng p c= A by RELAT_1:def_19;
A3: rng (f * p) c= D by RELAT_1:def_19;
dom f = A by A1, FUNCT_2:def_1;
then f * p is FinSequence by A2, FINSEQ_1:16;
hence f * p is FinSequence of D by A3, FINSEQ_1:def_4; ::_thesis: verum
end;
end;
end;
theorem Th33: :: FINSEQ_2:33
for A being set
for D9 being non empty set
for q being FinSequence
for p being FinSequence of A
for f being Function of A,D9 st q = f * p holds
len q = len p
proof
let A be set ; ::_thesis: for D9 being non empty set
for q being FinSequence
for p being FinSequence of A
for f being Function of A,D9 st q = f * p holds
len q = len p
let D9 be non empty set ; ::_thesis: for q being FinSequence
for p being FinSequence of A
for f being Function of A,D9 st q = f * p holds
len q = len p
let q be FinSequence; ::_thesis: for p being FinSequence of A
for f being Function of A,D9 st q = f * p holds
len q = len p
let p be FinSequence of A; ::_thesis: for f being Function of A,D9 st q = f * p holds
len q = len p
let f be Function of A,D9; ::_thesis: ( q = f * p implies len q = len p )
( dom f = A & rng p c= A ) by FINSEQ_1:def_4, FUNCT_2:def_1;
hence ( q = f * p implies len q = len p ) by Th29; ::_thesis: verum
end;
theorem :: FINSEQ_2:34
for x being set
for f being Function st x in dom f holds
f * <*x*> = <*(f . x)*>
proof
let x be set ; ::_thesis: for f being Function st x in dom f holds
f * <*x*> = <*(f . x)*>
let f be Function; ::_thesis: ( x in dom f implies f * <*x*> = <*(f . x)*> )
assume A1: x in dom f ; ::_thesis: f * <*x*> = <*(f . x)*>
then reconsider D = dom f, E = rng f as non empty set by FUNCT_1:3;
rng <*x*> = {x} by FINSEQ_1:38;
then rng <*x*> c= D by A1, ZFMISC_1:31;
then reconsider p = <*x*> as FinSequence of D by FINSEQ_1:def_4;
reconsider f = f as Function of D,E by FUNCT_2:def_1, RELSET_1:4;
reconsider q = f * p as FinSequence of E by Th32;
A2: p . 1 = x by FINSEQ_1:40;
A3: len q = len p by Th33
.= 1 by FINSEQ_1:39 ;
then 1 in Seg (len q) ;
then 1 in dom q by FINSEQ_1:def_3;
then q . 1 = f . x by A2, FUNCT_1:12;
hence f * <*x*> = <*(f . x)*> by A3, FINSEQ_1:40; ::_thesis: verum
end;
theorem :: FINSEQ_2:35
for x1 being set
for D, D9 being non empty set
for p being FinSequence of D
for f being Function of D,D9 st p = <*x1*> holds
f * p = <*(f . x1)*>
proof
let x1 be set ; ::_thesis: for D, D9 being non empty set
for p being FinSequence of D
for f being Function of D,D9 st p = <*x1*> holds
f * p = <*(f . x1)*>
let D, D9 be non empty set ; ::_thesis: for p being FinSequence of D
for f being Function of D,D9 st p = <*x1*> holds
f * p = <*(f . x1)*>
let p be FinSequence of D; ::_thesis: for f being Function of D,D9 st p = <*x1*> holds
f * p = <*(f . x1)*>
let f be Function of D,D9; ::_thesis: ( p = <*x1*> implies f * p = <*(f . x1)*> )
assume A1: p = <*x1*> ; ::_thesis: f * p = <*(f . x1)*>
A2: p . 1 = x1 by A1, FINSEQ_1:40;
reconsider q = f * p as FinSequence of D9 by Th32;
len p = 1 by A1, FINSEQ_1:39;
then A3: len q = 1 by Th33;
then 1 in Seg (len q) ;
then 1 in dom q by FINSEQ_1:def_3;
then q . 1 = f . x1 by A2, FUNCT_1:12;
hence f * p = <*(f . x1)*> by A3, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th36: :: FINSEQ_2:36
for x1, x2 being set
for D, D9 being non empty set
for p being FinSequence of D
for f being Function of D,D9 st p = <*x1,x2*> holds
f * p = <*(f . x1),(f . x2)*>
proof
let x1, x2 be set ; ::_thesis: for D, D9 being non empty set
for p being FinSequence of D
for f being Function of D,D9 st p = <*x1,x2*> holds
f * p = <*(f . x1),(f . x2)*>
let D, D9 be non empty set ; ::_thesis: for p being FinSequence of D
for f being Function of D,D9 st p = <*x1,x2*> holds
f * p = <*(f . x1),(f . x2)*>
let p be FinSequence of D; ::_thesis: for f being Function of D,D9 st p = <*x1,x2*> holds
f * p = <*(f . x1),(f . x2)*>
let f be Function of D,D9; ::_thesis: ( p = <*x1,x2*> implies f * p = <*(f . x1),(f . x2)*> )
assume A1: p = <*x1,x2*> ; ::_thesis: f * p = <*(f . x1),(f . x2)*>
A2: p . 2 = x2 by A1, FINSEQ_1:44;
reconsider q = f * p as FinSequence of D9 by Th32;
len p = 2 by A1, FINSEQ_1:44;
then A3: len q = 2 by Th33;
then 2 in Seg (len q) ;
then 2 in dom q by FINSEQ_1:def_3;
then A4: q . 2 = f . x2 by A2, FUNCT_1:12;
1 in Seg (len q) by A3;
then A5: 1 in dom q by FINSEQ_1:def_3;
p . 1 = x1 by A1, FINSEQ_1:44;
then q . 1 = f . x1 by A5, FUNCT_1:12;
hence f * p = <*(f . x1),(f . x2)*> by A3, A4, FINSEQ_1:44; ::_thesis: verum
end;
theorem Th37: :: FINSEQ_2:37
for x1, x2, x3 being set
for D, D9 being non empty set
for p being FinSequence of D
for f being Function of D,D9 st p = <*x1,x2,x3*> holds
f * p = <*(f . x1),(f . x2),(f . x3)*>
proof
let x1, x2, x3 be set ; ::_thesis: for D, D9 being non empty set
for p being FinSequence of D
for f being Function of D,D9 st p = <*x1,x2,x3*> holds
f * p = <*(f . x1),(f . x2),(f . x3)*>
let D, D9 be non empty set ; ::_thesis: for p being FinSequence of D
for f being Function of D,D9 st p = <*x1,x2,x3*> holds
f * p = <*(f . x1),(f . x2),(f . x3)*>
let p be FinSequence of D; ::_thesis: for f being Function of D,D9 st p = <*x1,x2,x3*> holds
f * p = <*(f . x1),(f . x2),(f . x3)*>
let f be Function of D,D9; ::_thesis: ( p = <*x1,x2,x3*> implies f * p = <*(f . x1),(f . x2),(f . x3)*> )
assume A1: p = <*x1,x2,x3*> ; ::_thesis: f * p = <*(f . x1),(f . x2),(f . x3)*>
A2: p . 2 = x2 by A1, FINSEQ_1:45;
reconsider q = f * p as FinSequence of D9 by Th32;
len p = 3 by A1, FINSEQ_1:45;
then A3: len q = 3 by Th33;
then 2 in Seg (len q) ;
then 2 in dom q by FINSEQ_1:def_3;
then A4: q . 2 = f . x2 by A2, FUNCT_1:12;
A5: p . 3 = x3 by A1, FINSEQ_1:45;
A6: p . 1 = x1 by A1, FINSEQ_1:45;
3 in Seg (len q) by A3;
then 3 in dom q by FINSEQ_1:def_3;
then A7: q . 3 = f . x3 by A5, FUNCT_1:12;
1 in Seg (len q) by A3;
then 1 in dom q by FINSEQ_1:def_3;
then q . 1 = f . x1 by A6, FUNCT_1:12;
hence f * p = <*(f . x1),(f . x2),(f . x3)*> by A3, A4, A7, FINSEQ_1:45; ::_thesis: verum
end;
theorem Th38: :: FINSEQ_2:38
for i, j being Nat
for p being FinSequence
for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds
p * f is FinSequence
proof
let i, j be Nat; ::_thesis: for p being FinSequence
for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds
p * f is FinSequence
let p be FinSequence; ::_thesis: for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds
p * f is FinSequence
let f be Function of (Seg i),(Seg j); ::_thesis: ( ( j = 0 implies i = 0 ) & j <= len p implies p * f is FinSequence )
assume ( j = 0 implies i = 0 ) ; ::_thesis: ( not j <= len p or p * f is FinSequence )
then ( Seg j = {} implies Seg i = {} ) ;
then A1: dom f = Seg i by FUNCT_2:def_1;
assume j <= len p ; ::_thesis: p * f is FinSequence
then ( rng f c= Seg j & Seg j c= Seg (len p) ) by FINSEQ_1:5, RELAT_1:def_19;
then rng f c= Seg (len p) by XBOOLE_1:1;
then rng f c= dom p by FINSEQ_1:def_3;
then dom (p * f) = dom f by RELAT_1:27;
hence p * f is FinSequence by A1, FINSEQ_1:def_2; ::_thesis: verum
end;
theorem :: FINSEQ_2:39
for i being Nat
for p being FinSequence
for f being Function of (Seg i),(Seg i) st i <= len p holds
p * f is FinSequence by Th38;
theorem :: FINSEQ_2:40
for p being FinSequence
for f being Function of (dom p),(dom p) holds p * f is FinSequence
proof
let p be FinSequence; ::_thesis: for f being Function of (dom p),(dom p) holds p * f is FinSequence
dom p = Seg (len p) by FINSEQ_1:def_3;
hence for f being Function of (dom p),(dom p) holds p * f is FinSequence by Th38; ::_thesis: verum
end;
theorem Th41: :: FINSEQ_2:41
for i being Nat
for p, q being FinSequence
for f being Function of (Seg i),(Seg i) st rng f = Seg i & i <= len p & q = p * f holds
len q = i
proof
let i be Nat; ::_thesis: for p, q being FinSequence
for f being Function of (Seg i),(Seg i) st rng f = Seg i & i <= len p & q = p * f holds
len q = i
let p, q be FinSequence; ::_thesis: for f being Function of (Seg i),(Seg i) st rng f = Seg i & i <= len p & q = p * f holds
len q = i
let f be Function of (Seg i),(Seg i); ::_thesis: ( rng f = Seg i & i <= len p & q = p * f implies len q = i )
assume ( rng f = Seg i & i <= len p ) ; ::_thesis: ( not q = p * f or len q = i )
then rng f c= Seg (len p) by FINSEQ_1:5;
then rng f c= dom p by FINSEQ_1:def_3;
then A1: dom (p * f) = dom f by RELAT_1:27;
( i is Element of NAT & dom f = Seg i ) by FUNCT_2:52, ORDINAL1:def_12;
hence ( not q = p * f or len q = i ) by A1, FINSEQ_1:def_3; ::_thesis: verum
end;
theorem Th42: :: FINSEQ_2:42
for p, q being FinSequence
for f being Function of (dom p),(dom p) st rng f = dom p & q = p * f holds
len q = len p
proof
let p, q be FinSequence; ::_thesis: for f being Function of (dom p),(dom p) st rng f = dom p & q = p * f holds
len q = len p
Seg (len p) = dom p by FINSEQ_1:def_3;
hence for f being Function of (dom p),(dom p) st rng f = dom p & q = p * f holds
len q = len p by Th41; ::_thesis: verum
end;
theorem Th43: :: FINSEQ_2:43
for i being Nat
for p, q being FinSequence
for f being Permutation of (Seg i) st i <= len p & q = p * f holds
len q = i
proof
let i be Nat; ::_thesis: for p, q being FinSequence
for f being Permutation of (Seg i) st i <= len p & q = p * f holds
len q = i
let p, q be FinSequence; ::_thesis: for f being Permutation of (Seg i) st i <= len p & q = p * f holds
len q = i
let f be Permutation of (Seg i); ::_thesis: ( i <= len p & q = p * f implies len q = i )
rng f = Seg i by FUNCT_2:def_3;
hence ( i <= len p & q = p * f implies len q = i ) by Th41; ::_thesis: verum
end;
theorem :: FINSEQ_2:44
for p, q being FinSequence
for f being Permutation of (dom p) st q = p * f holds
len q = len p
proof
let p, q be FinSequence; ::_thesis: for f being Permutation of (dom p) st q = p * f holds
len q = len p
Seg (len p) = dom p by FINSEQ_1:def_3;
hence for f being Permutation of (dom p) st q = p * f holds
len q = len p by Th43; ::_thesis: verum
end;
theorem Th45: :: FINSEQ_2:45
for i, j being Nat
for D being non empty set
for p being FinSequence of D
for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds
p * f is FinSequence of D
proof
let i, j be Nat; ::_thesis: for D being non empty set
for p being FinSequence of D
for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds
p * f is FinSequence of D
let D be non empty set ; ::_thesis: for p being FinSequence of D
for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds
p * f is FinSequence of D
let p be FinSequence of D; ::_thesis: for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds
p * f is FinSequence of D
let f be Function of (Seg i),(Seg j); ::_thesis: ( ( j = 0 implies i = 0 ) & j <= len p implies p * f is FinSequence of D )
assume A1: ( ( j = 0 implies i = 0 ) & j <= len p ) ; ::_thesis: p * f is FinSequence of D
set q = p * f;
( rng p c= D & rng (p * f) c= rng p ) by FINSEQ_1:def_4, RELAT_1:26;
then A2: rng (p * f) c= D by XBOOLE_1:1;
p * f is FinSequence by A1, Th38;
hence p * f is FinSequence of D by A2, FINSEQ_1:def_4; ::_thesis: verum
end;
theorem :: FINSEQ_2:46
for i being Nat
for D being non empty set
for p being FinSequence of D
for f being Function of (Seg i),(Seg i) st i <= len p holds
p * f is FinSequence of D by Th45;
theorem Th47: :: FINSEQ_2:47
for D being non empty set
for p being FinSequence of D
for f being Function of (dom p),(dom p) holds p * f is FinSequence of D
proof
let D be non empty set ; ::_thesis: for p being FinSequence of D
for f being Function of (dom p),(dom p) holds p * f is FinSequence of D
let p be FinSequence of D; ::_thesis: for f being Function of (dom p),(dom p) holds p * f is FinSequence of D
Seg (len p) = dom p by FINSEQ_1:def_3;
hence for f being Function of (dom p),(dom p) holds p * f is FinSequence of D by Th45; ::_thesis: verum
end;
theorem Th48: :: FINSEQ_2:48
for k being Nat holds id (Seg k) is FinSequence of NAT
proof
let k be Nat; ::_thesis: id (Seg k) is FinSequence of NAT
set I = id (Seg k);
reconsider k = k as Element of NAT by ORDINAL1:def_12;
dom (id (Seg k)) = Seg k ;
then ( rng (id (Seg k)) = Seg k & id (Seg k) is FinSequence ) by FINSEQ_1:def_2;
hence id (Seg k) is FinSequence of NAT by FINSEQ_1:def_4; ::_thesis: verum
end;
definition
let i be Nat;
func idseq i -> FinSequence equals :: FINSEQ_2:def 1
id (Seg i);
coherence
id (Seg i) is FinSequence by Th48;
end;
:: deftheorem defines idseq FINSEQ_2:def_1_:_
for i being Nat holds idseq i = id (Seg i);
registration
let k be Nat;
cluster idseq k -> k -element ;
coherence
idseq k is k -element
proof
( k in NAT & dom (idseq k) = Seg k ) by ORDINAL1:def_12, RELAT_1:45;
hence len (idseq k) = k by FINSEQ_1:def_3; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;
registration
cluster idseq 0 -> empty ;
coherence
idseq 0 is empty ;
end;
theorem :: FINSEQ_2:49
for i being Nat
for k being Element of Seg i holds (idseq i) . k = k
proof
let i be Nat; ::_thesis: for k being Element of Seg i holds (idseq i) . k = k
let k be Element of Seg i; ::_thesis: (idseq i) . k = k
percases ( i <> 0 or i = 0 ) ;
suppose i <> 0 ; ::_thesis: (idseq i) . k = k
hence (idseq i) . k = k by FUNCT_1:18; ::_thesis: verum
end;
suppose i = 0 ; ::_thesis: (idseq i) . k = k
then ( k = 0 & dom (idseq i) = 0 ) by SUBSET_1:def_1;
hence (idseq i) . k = k by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
theorem Th50: :: FINSEQ_2:50
idseq 1 = <*1*>
proof
1 in Seg 1 ;
then ( len (idseq 1) = 1 & (idseq 1) . 1 = 1 ) by CARD_1:def_7, FUNCT_1:18;
hence idseq 1 = <*1*> by FINSEQ_1:40; ::_thesis: verum
end;
theorem Th51: :: FINSEQ_2:51
for i being Nat holds idseq (i + 1) = (idseq i) ^ <*(i + 1)*>
proof
let i be Nat; ::_thesis: idseq (i + 1) = (idseq i) ^ <*(i + 1)*>
set p = idseq (i + 1);
consider q being FinSequence, a being set such that
A1: idseq (i + 1) = q ^ <*a*> by FINSEQ_1:46;
A2: ( len (idseq (i + 1)) = i + 1 & len (idseq (i + 1)) = (len q) + 1 ) by A1, Th16, CARD_1:def_7;
A3: dom q = Seg (len q) by FINSEQ_1:def_3;
A4: for a being set st a in Seg i holds
q . a = a
proof
i <= i + 1 by NAT_1:11;
then A5: Seg i c= Seg (i + 1) by FINSEQ_1:5;
let a be set ; ::_thesis: ( a in Seg i implies q . a = a )
assume A6: a in Seg i ; ::_thesis: q . a = a
then reconsider j = a as Element of NAT ;
(idseq (i + 1)) . j = q . j by A1, A2, A3, A6, FINSEQ_1:def_7;
hence q . a = a by A6, A5, FUNCT_1:18; ::_thesis: verum
end;
(idseq (i + 1)) . (i + 1) = i + 1 by FINSEQ_1:4, FUNCT_1:18;
then a = i + 1 by A1, A2, FINSEQ_1:42;
hence idseq (i + 1) = (idseq i) ^ <*(i + 1)*> by A1, A2, A3, A4, FUNCT_1:17; ::_thesis: verum
end;
theorem Th52: :: FINSEQ_2:52
idseq 2 = <*1,2*> by Th50, Th51;
theorem :: FINSEQ_2:53
idseq 3 = <*1,2,3*> by Th51, Th52;
theorem Th54: :: FINSEQ_2:54
for k being Nat
for p being FinSequence st len p <= k holds
p * (idseq k) = p
proof
let k be Nat; ::_thesis: for p being FinSequence st len p <= k holds
p * (idseq k) = p
let p be FinSequence; ::_thesis: ( len p <= k implies p * (idseq k) = p )
assume A1: len p <= k ; ::_thesis: p * (idseq k) = p
reconsider k = k as Element of NAT by ORDINAL1:def_12;
dom p = Seg (len p) by FINSEQ_1:def_3;
then dom p c= Seg k by A1, FINSEQ_1:5;
hence p * (idseq k) = p by RELAT_1:51; ::_thesis: verum
end;
theorem :: FINSEQ_2:55
for k being Nat holds idseq k is Permutation of (Seg k) ;
theorem Th56: :: FINSEQ_2:56
for k being Nat
for a being set holds (Seg k) --> a is FinSequence
proof
let k be Nat; ::_thesis: for a being set holds (Seg k) --> a is FinSequence
let a be set ; ::_thesis: (Seg k) --> a is FinSequence
set p = (Seg k) --> a;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
dom ((Seg k) --> a) = Seg k by FUNCOP_1:13;
hence (Seg k) --> a is FinSequence by FINSEQ_1:def_2; ::_thesis: verum
end;
registration
let k be Nat;
let a be set ;
cluster(Seg k) --> a -> FinSequence-like ;
coherence
(Seg k) --> a is FinSequence-like by Th56;
end;
definition
let i be Nat;
let a be set ;
funci |-> a -> FinSequence equals :: FINSEQ_2:def 2
(Seg i) --> a;
coherence
(Seg i) --> a is FinSequence ;
end;
:: deftheorem defines |-> FINSEQ_2:def_2_:_
for i being Nat
for a being set holds i |-> a = (Seg i) --> a;
registration
let k be Nat;
let a be set ;
clusterk |-> a -> k -element ;
coherence
k |-> a is k -element
proof
( k in NAT & dom (k |-> a) = Seg k ) by FUNCOP_1:13, ORDINAL1:def_12;
hence len (k |-> a) = k by FINSEQ_1:def_3; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;
theorem Th57: :: FINSEQ_2:57
for k being Nat
for d, w being set st w in Seg k holds
(k |-> d) . w = d by FUNCOP_1:7;
theorem :: FINSEQ_2:58
for a being set holds 0 |-> a = {} ;
theorem Th59: :: FINSEQ_2:59
for a being set holds 1 |-> a = <*a*>
proof
let a be set ; ::_thesis: 1 |-> a = <*a*>
1 in Seg 1 ;
then ( len (1 |-> a) = 1 & (1 |-> a) . 1 = a ) by CARD_1:def_7, FUNCOP_1:7;
hence 1 |-> a = <*a*> by FINSEQ_1:40; ::_thesis: verum
end;
theorem Th60: :: FINSEQ_2:60
for i being Nat
for a being set holds (i + 1) |-> a = (i |-> a) ^ <*a*>
proof
let i be Nat; ::_thesis: for a being set holds (i + 1) |-> a = (i |-> a) ^ <*a*>
let a be set ; ::_thesis: (i + 1) |-> a = (i |-> a) ^ <*a*>
set p = (i + 1) |-> a;
consider q being FinSequence, x being set such that
A1: (i + 1) |-> a = q ^ <*x*> by FINSEQ_1:46;
A2: ( len ((i + 1) |-> a) = i + 1 & len ((i + 1) |-> a) = (len q) + 1 ) by A1, Th16, CARD_1:def_7;
A3: now__::_thesis:_q_=_i_|->_a
percases ( i = 0 or i <> 0 ) ;
supposeA4: i = 0 ; ::_thesis: q = i |-> a
then q = {} by A2;
hence q = i |-> a by A4; ::_thesis: verum
end;
supposeA5: i <> 0 ; ::_thesis: q = i |-> a
A6: ( rng q c= rng ((i + 1) |-> a) & rng ((i + 1) |-> a) = {a} ) by A1, FINSEQ_1:29, FUNCOP_1:8;
A7: dom q = Seg (len q) by FINSEQ_1:def_3;
then i in dom q by A2, A5, FINSEQ_1:3;
then q . i in rng q by FUNCT_1:def_3;
then rng q = {a} by A6, ZFMISC_1:33;
hence q = i |-> a by A2, A7, FUNCOP_1:9; ::_thesis: verum
end;
end;
end;
((i + 1) |-> a) . (i + 1) = a by FINSEQ_1:4, FUNCOP_1:7;
hence (i + 1) |-> a = (i |-> a) ^ <*a*> by A1, A2, A3, FINSEQ_1:42; ::_thesis: verum
end;
theorem Th61: :: FINSEQ_2:61
for a being set holds 2 |-> a = <*a,a*>
proof
let a be set ; ::_thesis: 2 |-> a = <*a,a*>
thus 2 |-> a = (1 + 1) |-> a
.= (1 |-> a) ^ <*a*> by Th60
.= <*a,a*> by Th59 ; ::_thesis: verum
end;
theorem :: FINSEQ_2:62
for a being set holds 3 |-> a = <*a,a,a*>
proof
let a be set ; ::_thesis: 3 |-> a = <*a,a,a*>
thus 3 |-> a = (2 + 1) |-> a
.= (2 |-> a) ^ <*a*> by Th60
.= <*a,a*> ^ <*a*> by Th61
.= <*a,a,a*> ; ::_thesis: verum
end;
theorem Th63: :: FINSEQ_2:63
for k being Nat
for D being non empty set
for d being Element of D holds k |-> d is FinSequence of D
proof
let k be Nat; ::_thesis: for D being non empty set
for d being Element of D holds k |-> d is FinSequence of D
let D be non empty set ; ::_thesis: for d being Element of D holds k |-> d is FinSequence of D
let d be Element of D; ::_thesis: k |-> d is FinSequence of D
set s = k |-> d;
rng (k |-> d) c= {d} by FUNCOP_1:13;
then rng (k |-> d) c= D by XBOOLE_1:1;
hence k |-> d is FinSequence of D by FINSEQ_1:def_4; ::_thesis: verum
end;
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
proof
let i be Nat; ::_thesis: 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
let p, q be FinSequence; ::_thesis: 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
let F be Function; ::_thesis: ( [:(rng p),(rng q):] c= dom F & i = min ((len p),(len q)) implies dom (F .: (p,q)) = Seg i )
assume that
A1: [:(rng p),(rng q):] c= dom F and
A2: i = min ((len p),(len q)) ; ::_thesis: dom (F .: (p,q)) = Seg i
A3: ( rng <:p,q:> c= [:(rng p),(rng q):] & dom <:p,q:> = (dom p) /\ (dom q) ) by FUNCT_3:51, FUNCT_3:def_7;
( dom p = Seg (len p) & dom q = Seg (len q) ) by FINSEQ_1:def_3;
then (dom p) /\ (dom q) = Seg i by A2, Th2;
hence dom (F .: (p,q)) = Seg i by A1, A3, RELAT_1:27, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th64: :: FINSEQ_2:64
for p, q being FinSequence
for F being Function st [:(rng p),(rng q):] c= dom F holds
F .: (p,q) is FinSequence
proof
let p, q be FinSequence; ::_thesis: for F being Function st [:(rng p),(rng q):] c= dom F holds
F .: (p,q) is FinSequence
let F be Function; ::_thesis: ( [:(rng p),(rng q):] c= dom F implies F .: (p,q) is FinSequence )
reconsider k = min ((len p),(len q)) as Element of NAT by XXREAL_0:15;
assume [:(rng p),(rng q):] c= dom F ; ::_thesis: F .: (p,q) is FinSequence
then dom (F .: (p,q)) = Seg k by Lm3;
hence F .: (p,q) is FinSequence by FINSEQ_1:def_2; ::_thesis: verum
end;
theorem Th65: :: FINSEQ_2:65
for p, q, r being FinSequence
for F being Function st [:(rng p),(rng q):] c= dom F & r = F .: (p,q) holds
len r = min ((len p),(len q))
proof
let p, q, r be FinSequence; ::_thesis: for F being Function st [:(rng p),(rng q):] c= dom F & r = F .: (p,q) holds
len r = min ((len p),(len q))
let F be Function; ::_thesis: ( [:(rng p),(rng q):] c= dom F & r = F .: (p,q) implies len r = min ((len p),(len q)) )
reconsider k = min ((len p),(len q)) as Element of NAT by XXREAL_0:15;
assume [:(rng p),(rng q):] c= dom F ; ::_thesis: ( not r = F .: (p,q) or len r = min ((len p),(len q)) )
then dom (F .: (p,q)) = Seg k by Lm3;
hence ( not r = F .: (p,q) or len r = min ((len p),(len q)) ) by FINSEQ_1:def_3; ::_thesis: verum
end;
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
proof
let a be set ; ::_thesis: for p being FinSequence
for F being Function st [:{a},(rng p):] c= dom F holds
dom (F [;] (a,p)) = dom p
let p be FinSequence; ::_thesis: for F being Function st [:{a},(rng p):] c= dom F holds
dom (F [;] (a,p)) = dom p
let F be Function; ::_thesis: ( [:{a},(rng p):] c= dom F implies dom (F [;] (a,p)) = dom p )
assume A1: [:{a},(rng p):] c= dom F ; ::_thesis: dom (F [;] (a,p)) = dom p
set q = (dom p) --> a;
dom ((dom p) --> a) = dom p by FUNCOP_1:13;
then A2: dom <:((dom p) --> a),p:> = dom p by FUNCT_3:50;
rng ((dom p) --> a) c= {a} by FUNCOP_1:13;
then ( rng <:((dom p) --> a),p:> c= [:(rng ((dom p) --> a)),(rng p):] & [:(rng ((dom p) --> a)),(rng p):] c= [:{a},(rng p):] ) by FUNCT_3:51, ZFMISC_1:95;
then A3: rng <:((dom p) --> a),p:> c= [:{a},(rng p):] by XBOOLE_1:1;
thus dom (F [;] (a,p)) = dom p by A1, A3, A2, RELAT_1:27, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th66: :: FINSEQ_2:66
for a being set
for p being FinSequence
for F being Function st [:{a},(rng p):] c= dom F holds
F [;] (a,p) is FinSequence
proof
let a be set ; ::_thesis: for p being FinSequence
for F being Function st [:{a},(rng p):] c= dom F holds
F [;] (a,p) is FinSequence
let p be FinSequence; ::_thesis: for F being Function st [:{a},(rng p):] c= dom F holds
F [;] (a,p) is FinSequence
let F be Function; ::_thesis: ( [:{a},(rng p):] c= dom F implies F [;] (a,p) is FinSequence )
assume [:{a},(rng p):] c= dom F ; ::_thesis: F [;] (a,p) is FinSequence
then dom (F [;] (a,p)) = dom p by Lm4;
then dom (F [;] (a,p)) = Seg (len p) by FINSEQ_1:def_3;
hence F [;] (a,p) is FinSequence by FINSEQ_1:def_2; ::_thesis: verum
end;
theorem Th67: :: FINSEQ_2:67
for a being set
for p, r being FinSequence
for F being Function st [:{a},(rng p):] c= dom F & r = F [;] (a,p) holds
len r = len p
proof
let a be set ; ::_thesis: for p, r being FinSequence
for F being Function st [:{a},(rng p):] c= dom F & r = F [;] (a,p) holds
len r = len p
let p, r be FinSequence; ::_thesis: for F being Function st [:{a},(rng p):] c= dom F & r = F [;] (a,p) holds
len r = len p
let F be Function; ::_thesis: ( [:{a},(rng p):] c= dom F & r = F [;] (a,p) implies len r = len p )
assume [:{a},(rng p):] c= dom F ; ::_thesis: ( not r = F [;] (a,p) or len r = len p )
then dom (F [;] (a,p)) = dom p by Lm4;
then dom (F [;] (a,p)) = Seg (len p) by FINSEQ_1:def_3;
hence ( not r = F [;] (a,p) or len r = len p ) by FINSEQ_1:def_3; ::_thesis: verum
end;
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
proof
let a be set ; ::_thesis: for p being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F holds
dom (F [:] (p,a)) = dom p
let p be FinSequence; ::_thesis: for F being Function st [:(rng p),{a}:] c= dom F holds
dom (F [:] (p,a)) = dom p
let F be Function; ::_thesis: ( [:(rng p),{a}:] c= dom F implies dom (F [:] (p,a)) = dom p )
assume A1: [:(rng p),{a}:] c= dom F ; ::_thesis: dom (F [:] (p,a)) = dom p
set q = (dom p) --> a;
dom ((dom p) --> a) = dom p by FUNCOP_1:13;
then A2: dom <:p,((dom p) --> a):> = dom p by FUNCT_3:50;
rng ((dom p) --> a) c= {a} by FUNCOP_1:13;
then ( rng <:p,((dom p) --> a):> c= [:(rng p),(rng ((dom p) --> a)):] & [:(rng p),(rng ((dom p) --> a)):] c= [:(rng p),{a}:] ) by FUNCT_3:51, ZFMISC_1:95;
then A3: rng <:p,((dom p) --> a):> c= [:(rng p),{a}:] by XBOOLE_1:1;
thus dom (F [:] (p,a)) = dom p by A1, A3, A2, RELAT_1:27, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th68: :: FINSEQ_2:68
for a being set
for p being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F holds
F [:] (p,a) is FinSequence
proof
let a be set ; ::_thesis: for p being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F holds
F [:] (p,a) is FinSequence
let p be FinSequence; ::_thesis: for F being Function st [:(rng p),{a}:] c= dom F holds
F [:] (p,a) is FinSequence
let F be Function; ::_thesis: ( [:(rng p),{a}:] c= dom F implies F [:] (p,a) is FinSequence )
assume [:(rng p),{a}:] c= dom F ; ::_thesis: F [:] (p,a) is FinSequence
then dom (F [:] (p,a)) = dom p by Lm5;
then dom (F [:] (p,a)) = Seg (len p) by FINSEQ_1:def_3;
hence F [:] (p,a) is FinSequence by FINSEQ_1:def_2; ::_thesis: verum
end;
theorem Th69: :: FINSEQ_2:69
for a being set
for p, r being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F & r = F [:] (p,a) holds
len r = len p
proof
let a be set ; ::_thesis: for p, r being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F & r = F [:] (p,a) holds
len r = len p
let p, r be FinSequence; ::_thesis: for F being Function st [:(rng p),{a}:] c= dom F & r = F [:] (p,a) holds
len r = len p
let F be Function; ::_thesis: ( [:(rng p),{a}:] c= dom F & r = F [:] (p,a) implies len r = len p )
assume [:(rng p),{a}:] c= dom F ; ::_thesis: ( not r = F [:] (p,a) or len r = len p )
then dom (F [:] (p,a)) = dom p by Lm5;
then dom (F [:] (p,a)) = Seg (len p) by FINSEQ_1:def_3;
hence ( not r = F [:] (p,a) or len r = len p ) by FINSEQ_1:def_3; ::_thesis: verum
end;
theorem Th70: :: FINSEQ_2:70
for D, D9, E being non empty set
for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 holds F .: (p,q) is FinSequence of E
proof
let D, D9, E be non empty set ; ::_thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 holds F .: (p,q) is FinSequence of E
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D
for q being FinSequence of D9 holds F .: (p,q) is FinSequence of E
let p be FinSequence of D; ::_thesis: for q being FinSequence of D9 holds F .: (p,q) is FinSequence of E
let q be FinSequence of D9; ::_thesis: F .: (p,q) is FinSequence of E
A1: rng (F .: (p,q)) c= rng F by RELAT_1:26;
( rng p c= D & rng q c= D9 ) by FINSEQ_1:def_4;
then [:(rng p),(rng q):] c= [:D,D9:] by ZFMISC_1:96;
then [:(rng p),(rng q):] c= dom F by FUNCT_2:def_1;
then A2: F .: (p,q) is FinSequence by Th64;
rng F c= E by RELAT_1:def_19;
then rng (F .: (p,q)) c= E by A1, XBOOLE_1:1;
hence F .: (p,q) is FinSequence of E by A2, FINSEQ_1:def_4; ::_thesis: verum
end;
theorem Th71: :: FINSEQ_2:71
for D, D9, E being non empty set
for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 st r = F .: (p,q) holds
len r = min ((len p),(len q))
proof
let D, D9, E be non empty set ; ::_thesis: for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 st r = F .: (p,q) holds
len r = min ((len p),(len q))
let r be FinSequence; ::_thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 st r = F .: (p,q) holds
len r = min ((len p),(len q))
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D
for q being FinSequence of D9 st r = F .: (p,q) holds
len r = min ((len p),(len q))
let p be FinSequence of D; ::_thesis: for q being FinSequence of D9 st r = F .: (p,q) holds
len r = min ((len p),(len q))
let q be FinSequence of D9; ::_thesis: ( r = F .: (p,q) implies len r = min ((len p),(len q)) )
( rng p c= D & rng q c= D9 ) by FINSEQ_1:def_4;
then [:(rng p),(rng q):] c= [:D,D9:] by ZFMISC_1:96;
then [:(rng p),(rng q):] c= dom F by FUNCT_2:def_1;
hence ( r = F .: (p,q) implies len r = min ((len p),(len q)) ) by Th65; ::_thesis: verum
end;
theorem Th72: :: FINSEQ_2:72
for D, D9, E being non empty set
for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 st len p = len q & r = F .: (p,q) holds
( len r = len p & len r = len q )
proof
let D, D9, E be non empty set ; ::_thesis: for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 st len p = len q & r = F .: (p,q) holds
( len r = len p & len r = len q )
let r be FinSequence; ::_thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 st len p = len q & r = F .: (p,q) holds
( len r = len p & len r = len q )
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D
for q being FinSequence of D9 st len p = len q & r = F .: (p,q) holds
( len r = len p & len r = len q )
let p be FinSequence of D; ::_thesis: for q being FinSequence of D9 st len p = len q & r = F .: (p,q) holds
( len r = len p & len r = len q )
let q be FinSequence of D9; ::_thesis: ( len p = len q & r = F .: (p,q) implies ( len r = len p & len r = len q ) )
assume that
A1: len p = len q and
A2: r = F .: (p,q) ; ::_thesis: ( len r = len p & len r = len q )
len r = min ((len p),(len q)) by A2, Th71;
hence ( len r = len p & len r = len q ) by A1; ::_thesis: verum
end;
theorem :: FINSEQ_2:73
for D, D9, E being non empty set
for F being Function of [:D,D9:],E
for p being FinSequence of D
for p9 being FinSequence of D9 holds
( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E )
proof
let D, D9, E be non empty set ; ::_thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D
for p9 being FinSequence of D9 holds
( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E )
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D
for p9 being FinSequence of D9 holds
( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E )
let p be FinSequence of D; ::_thesis: for p9 being FinSequence of D9 holds
( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E )
let p9 be FinSequence of D9; ::_thesis: ( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E )
reconsider r = F .: ((<*> D),p9), r9 = F .: (p,(<*> D9)) as FinSequence of E by Th70;
len (<*> D) = 0 ;
then ( len r = min (0,(len p9)) & len r9 = min ((len p),0) ) by Th71;
hence ( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E ) by XXREAL_0:def_9; ::_thesis: verum
end;
theorem :: FINSEQ_2:74
for D, D9, E being non empty set
for d1 being Element of D
for d19 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*> & q = <*d19*> holds
F .: (p,q) = <*(F . (d1,d19))*>
proof
let D, D9, E be non empty set ; ::_thesis: for d1 being Element of D
for d19 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*> & q = <*d19*> holds
F .: (p,q) = <*(F . (d1,d19))*>
let d1 be Element of D; ::_thesis: for d19 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*> & q = <*d19*> holds
F .: (p,q) = <*(F . (d1,d19))*>
let d19 be Element of D9; ::_thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 st p = <*d1*> & q = <*d19*> holds
F .: (p,q) = <*(F . (d1,d19))*>
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D
for q being FinSequence of D9 st p = <*d1*> & q = <*d19*> holds
F .: (p,q) = <*(F . (d1,d19))*>
let p be FinSequence of D; ::_thesis: for q being FinSequence of D9 st p = <*d1*> & q = <*d19*> holds
F .: (p,q) = <*(F . (d1,d19))*>
let q be FinSequence of D9; ::_thesis: ( p = <*d1*> & q = <*d19*> implies F .: (p,q) = <*(F . (d1,d19))*> )
assume A1: ( p = <*d1*> & q = <*d19*> ) ; ::_thesis: F .: (p,q) = <*(F . (d1,d19))*>
A2: ( p . 1 = d1 & q . 1 = d19 ) by A1, FINSEQ_1:40;
reconsider r = F .: (p,q) as FinSequence of E by Th70;
( len p = 1 & len q = 1 ) by A1, FINSEQ_1:39;
then A3: len r = 1 by Th72;
then 1 in Seg (len r) ;
then 1 in dom r by FINSEQ_1:def_3;
then r . 1 = F . (d1,d19) by A2, FUNCOP_1:22;
hence F .: (p,q) = <*(F . (d1,d19))*> by A3, FINSEQ_1:40; ::_thesis: verum
end;
theorem :: FINSEQ_2:75
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))*>
proof
let D, D9, E be non empty set ; ::_thesis: 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))*>
let d1, d2 be Element of D; ::_thesis: 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))*>
let d19, d29 be Element of D9; ::_thesis: 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))*>
let F be Function of [:D,D9:],E; ::_thesis: 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))*>
let p be FinSequence of D; ::_thesis: for q being FinSequence of D9 st p = <*d1,d2*> & q = <*d19,d29*> holds
F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29))*>
let q be FinSequence of D9; ::_thesis: ( p = <*d1,d2*> & q = <*d19,d29*> implies F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29))*> )
assume A1: ( p = <*d1,d2*> & q = <*d19,d29*> ) ; ::_thesis: F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29))*>
A2: ( p . 2 = d2 & q . 2 = d29 ) by A1, FINSEQ_1:44;
reconsider r = F .: (p,q) as FinSequence of E by Th70;
( len p = 2 & len q = 2 ) by A1, FINSEQ_1:44;
then A3: len r = 2 by Th72;
then 2 in Seg (len r) ;
then 2 in dom r by FINSEQ_1:def_3;
then A4: r . 2 = F . (d2,d29) by A2, FUNCOP_1:22;
1 in Seg (len r) by A3;
then A5: 1 in dom r by FINSEQ_1:def_3;
( p . 1 = d1 & q . 1 = d19 ) by A1, FINSEQ_1:44;
then r . 1 = F . (d1,d19) by A5, FUNCOP_1:22;
hence F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29))*> by A3, A4, FINSEQ_1:44; ::_thesis: verum
end;
theorem :: FINSEQ_2:76
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))*>
proof
let D, D9, E be non empty set ; ::_thesis: 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))*>
let d1, d2, d3 be Element of D; ::_thesis: 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))*>
let d19, d29, d39 be Element of D9; ::_thesis: 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))*>
let F be Function of [:D,D9:],E; ::_thesis: 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))*>
let p be FinSequence of D; ::_thesis: 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))*>
let q be FinSequence of D9; ::_thesis: ( p = <*d1,d2,d3*> & q = <*d19,d29,d39*> implies F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29)),(F . (d3,d39))*> )
assume A1: ( p = <*d1,d2,d3*> & q = <*d19,d29,d39*> ) ; ::_thesis: F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29)),(F . (d3,d39))*>
A2: ( p . 2 = d2 & q . 2 = d29 ) by A1, FINSEQ_1:45;
reconsider r = F .: (p,q) as FinSequence of E by Th70;
( len p = 3 & len q = 3 ) by A1, FINSEQ_1:45;
then A3: len r = 3 by Th72;
then 2 in Seg (len r) ;
then 2 in dom r by FINSEQ_1:def_3;
then A4: r . 2 = F . (d2,d29) by A2, FUNCOP_1:22;
A5: ( p . 3 = d3 & q . 3 = d39 ) by A1, FINSEQ_1:45;
A6: ( p . 1 = d1 & q . 1 = d19 ) by A1, FINSEQ_1:45;
3 in Seg (len r) by A3;
then 3 in dom r by FINSEQ_1:def_3;
then A7: r . 3 = F . (d3,d39) by A5, FUNCOP_1:22;
1 in Seg (len r) by A3;
then 1 in dom r by FINSEQ_1:def_3;
then r . 1 = F . (d1,d19) by A6, FUNCOP_1:22;
hence F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29)),(F . (d3,d39))*> by A3, A4, A7, FINSEQ_1:45; ::_thesis: verum
end;
theorem Th77: :: FINSEQ_2:77
for D, D9, E being non empty set
for d being Element of D
for F being Function of [:D,D9:],E
for p being FinSequence of D9 holds F [;] (d,p) is FinSequence of E
proof
let D, D9, E be non empty set ; ::_thesis: for d being Element of D
for F being Function of [:D,D9:],E
for p being FinSequence of D9 holds F [;] (d,p) is FinSequence of E
let d be Element of D; ::_thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D9 holds F [;] (d,p) is FinSequence of E
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D9 holds F [;] (d,p) is FinSequence of E
let p be FinSequence of D9; ::_thesis: F [;] (d,p) is FinSequence of E
A1: rng (F [;] (d,p)) c= rng F by RELAT_1:26;
rng p c= D9 by FINSEQ_1:def_4;
then [:{d},(rng p):] c= [:D,D9:] by ZFMISC_1:96;
then [:{d},(rng p):] c= dom F by FUNCT_2:def_1;
then A2: F [;] (d,p) is FinSequence by Th66;
rng F c= E by RELAT_1:def_19;
then rng (F [;] (d,p)) c= E by A1, XBOOLE_1:1;
hence F [;] (d,p) is FinSequence of E by A2, FINSEQ_1:def_4; ::_thesis: verum
end;
theorem Th78: :: FINSEQ_2:78
for D, D9, E being non empty set
for d being Element of D
for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D9 st r = F [;] (d,p) holds
len r = len p
proof
let D, D9, E be non empty set ; ::_thesis: for d being Element of D
for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D9 st r = F [;] (d,p) holds
len r = len p
let d be Element of D; ::_thesis: for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D9 st r = F [;] (d,p) holds
len r = len p
let r be FinSequence; ::_thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D9 st r = F [;] (d,p) holds
len r = len p
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D9 st r = F [;] (d,p) holds
len r = len p
let p be FinSequence of D9; ::_thesis: ( r = F [;] (d,p) implies len r = len p )
rng p c= D9 by FINSEQ_1:def_4;
then [:{d},(rng p):] c= [:D,D9:] by ZFMISC_1:96;
then [:{d},(rng p):] c= dom F by FUNCT_2:def_1;
hence ( r = F [;] (d,p) implies len r = len p ) by Th67; ::_thesis: verum
end;
theorem :: FINSEQ_2:79
for D, D9, E being non empty set
for d being Element of D
for F being Function of [:D,D9:],E holds F [;] (d,(<*> D9)) = <*> E
proof
let D, D9, E be non empty set ; ::_thesis: for d being Element of D
for F being Function of [:D,D9:],E holds F [;] (d,(<*> D9)) = <*> E
let d be Element of D; ::_thesis: for F being Function of [:D,D9:],E holds F [;] (d,(<*> D9)) = <*> E
let F be Function of [:D,D9:],E; ::_thesis: F [;] (d,(<*> D9)) = <*> E
reconsider r = F [;] (d,(<*> D9)) as FinSequence of E by Th77;
len (<*> D9) = 0 ;
then len r = 0 by Th78;
hence F [;] (d,(<*> D9)) = <*> E ; ::_thesis: verum
end;
theorem :: FINSEQ_2:80
for D, D9, E being non empty set
for d being Element of D
for d19 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D9 st p = <*d19*> holds
F [;] (d,p) = <*(F . (d,d19))*>
proof
let D, D9, E be non empty set ; ::_thesis: for d being Element of D
for d19 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D9 st p = <*d19*> holds
F [;] (d,p) = <*(F . (d,d19))*>
let d be Element of D; ::_thesis: for d19 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D9 st p = <*d19*> holds
F [;] (d,p) = <*(F . (d,d19))*>
let d19 be Element of D9; ::_thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D9 st p = <*d19*> holds
F [;] (d,p) = <*(F . (d,d19))*>
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D9 st p = <*d19*> holds
F [;] (d,p) = <*(F . (d,d19))*>
let p be FinSequence of D9; ::_thesis: ( p = <*d19*> implies F [;] (d,p) = <*(F . (d,d19))*> )
assume A1: p = <*d19*> ; ::_thesis: F [;] (d,p) = <*(F . (d,d19))*>
A2: p . 1 = d19 by A1, FINSEQ_1:40;
reconsider r = F [;] (d,p) as FinSequence of E by Th77;
len p = 1 by A1, FINSEQ_1:39;
then A3: len r = 1 by Th78;
then 1 in Seg (len r) ;
then 1 in dom r by FINSEQ_1:def_3;
then r . 1 = F . (d,d19) by A2, FUNCOP_1:32;
hence F [;] (d,p) = <*(F . (d,d19))*> by A3, FINSEQ_1:40; ::_thesis: verum
end;
theorem :: FINSEQ_2:81
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))*>
proof
let D, D9, E be non empty set ; ::_thesis: 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))*>
let d be Element of D; ::_thesis: 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))*>
let d19, d29 be Element of D9; ::_thesis: 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))*>
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D9 st p = <*d19,d29*> holds
F [;] (d,p) = <*(F . (d,d19)),(F . (d,d29))*>
let p be FinSequence of D9; ::_thesis: ( p = <*d19,d29*> implies F [;] (d,p) = <*(F . (d,d19)),(F . (d,d29))*> )
assume A1: p = <*d19,d29*> ; ::_thesis: F [;] (d,p) = <*(F . (d,d19)),(F . (d,d29))*>
A2: p . 2 = d29 by A1, FINSEQ_1:44;
reconsider r = F [;] (d,p) as FinSequence of E by Th77;
len p = 2 by A1, FINSEQ_1:44;
then A3: len r = 2 by Th78;
then 2 in Seg (len r) ;
then 2 in dom r by FINSEQ_1:def_3;
then A4: r . 2 = F . (d,d29) by A2, FUNCOP_1:32;
1 in Seg (len r) by A3;
then A5: 1 in dom r by FINSEQ_1:def_3;
p . 1 = d19 by A1, FINSEQ_1:44;
then r . 1 = F . (d,d19) by A5, FUNCOP_1:32;
hence F [;] (d,p) = <*(F . (d,d19)),(F . (d,d29))*> by A3, A4, FINSEQ_1:44; ::_thesis: verum
end;
theorem :: FINSEQ_2:82
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))*>
proof
let D, D9, E be non empty set ; ::_thesis: 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))*>
let d be Element of D; ::_thesis: 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))*>
let d19, d29, d39 be Element of D9; ::_thesis: 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))*>
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D9 st p = <*d19,d29,d39*> holds
F [;] (d,p) = <*(F . (d,d19)),(F . (d,d29)),(F . (d,d39))*>
let p be FinSequence of D9; ::_thesis: ( p = <*d19,d29,d39*> implies F [;] (d,p) = <*(F . (d,d19)),(F . (d,d29)),(F . (d,d39))*> )
assume A1: p = <*d19,d29,d39*> ; ::_thesis: F [;] (d,p) = <*(F . (d,d19)),(F . (d,d29)),(F . (d,d39))*>
A2: p . 2 = d29 by A1, FINSEQ_1:45;
reconsider r = F [;] (d,p) as FinSequence of E by Th77;
len p = 3 by A1, FINSEQ_1:45;
then A3: len r = 3 by Th78;
then 2 in Seg (len r) ;
then 2 in dom r by FINSEQ_1:def_3;
then A4: r . 2 = F . (d,d29) by A2, FUNCOP_1:32;
A5: p . 3 = d39 by A1, FINSEQ_1:45;
A6: p . 1 = d19 by A1, FINSEQ_1:45;
3 in Seg (len r) by A3;
then 3 in dom r by FINSEQ_1:def_3;
then A7: r . 3 = F . (d,d39) by A5, FUNCOP_1:32;
1 in Seg (len r) by A3;
then 1 in dom r by FINSEQ_1:def_3;
then r . 1 = F . (d,d19) by A6, FUNCOP_1:32;
hence F [;] (d,p) = <*(F . (d,d19)),(F . (d,d29)),(F . (d,d39))*> by A3, A4, A7, FINSEQ_1:45; ::_thesis: verum
end;
theorem Th83: :: FINSEQ_2:83
for D, D9, E being non empty set
for d9 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D holds F [:] (p,d9) is FinSequence of E
proof
let D, D9, E be non empty set ; ::_thesis: for d9 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D holds F [:] (p,d9) is FinSequence of E
let d9 be Element of D9; ::_thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D holds F [:] (p,d9) is FinSequence of E
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D holds F [:] (p,d9) is FinSequence of E
let p be FinSequence of D; ::_thesis: F [:] (p,d9) is FinSequence of E
A1: rng (F [:] (p,d9)) c= rng F by RELAT_1:26;
rng p c= D by FINSEQ_1:def_4;
then [:(rng p),{d9}:] c= [:D,D9:] by ZFMISC_1:96;
then [:(rng p),{d9}:] c= dom F by FUNCT_2:def_1;
then A2: F [:] (p,d9) is FinSequence by Th68;
rng F c= E by RELAT_1:def_19;
then rng (F [:] (p,d9)) c= E by A1, XBOOLE_1:1;
hence F [:] (p,d9) is FinSequence of E by A2, FINSEQ_1:def_4; ::_thesis: verum
end;
theorem Th84: :: FINSEQ_2:84
for D, D9, E being non empty set
for d9 being Element of D9
for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D st r = F [:] (p,d9) holds
len r = len p
proof
let D, D9, E be non empty set ; ::_thesis: for d9 being Element of D9
for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D st r = F [:] (p,d9) holds
len r = len p
let d9 be Element of D9; ::_thesis: for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D st r = F [:] (p,d9) holds
len r = len p
let r be FinSequence; ::_thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D st r = F [:] (p,d9) holds
len r = len p
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D st r = F [:] (p,d9) holds
len r = len p
let p be FinSequence of D; ::_thesis: ( r = F [:] (p,d9) implies len r = len p )
rng p c= D by FINSEQ_1:def_4;
then [:(rng p),{d9}:] c= [:D,D9:] by ZFMISC_1:96;
then [:(rng p),{d9}:] c= dom F by FUNCT_2:def_1;
hence ( r = F [:] (p,d9) implies len r = len p ) by Th69; ::_thesis: verum
end;
theorem :: FINSEQ_2:85
for D, D9, E being non empty set
for d9 being Element of D9
for F being Function of [:D,D9:],E holds F [:] ((<*> D),d9) = <*> E
proof
let D, D9, E be non empty set ; ::_thesis: for d9 being Element of D9
for F being Function of [:D,D9:],E holds F [:] ((<*> D),d9) = <*> E
let d9 be Element of D9; ::_thesis: for F being Function of [:D,D9:],E holds F [:] ((<*> D),d9) = <*> E
let F be Function of [:D,D9:],E; ::_thesis: F [:] ((<*> D),d9) = <*> E
reconsider r = F [:] ((<*> D),d9) as FinSequence of E by Th83;
len (<*> D) = 0 ;
then len r = 0 by Th84;
hence F [:] ((<*> D),d9) = <*> E ; ::_thesis: verum
end;
theorem :: FINSEQ_2:86
for D, D9, E being non empty set
for d1 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*> holds
F [:] (p,d9) = <*(F . (d1,d9))*>
proof
let D, D9, E be non empty set ; ::_thesis: for d1 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*> holds
F [:] (p,d9) = <*(F . (d1,d9))*>
let d1 be Element of D; ::_thesis: for d9 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D st p = <*d1*> holds
F [:] (p,d9) = <*(F . (d1,d9))*>
let d9 be Element of D9; ::_thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D st p = <*d1*> holds
F [:] (p,d9) = <*(F . (d1,d9))*>
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D st p = <*d1*> holds
F [:] (p,d9) = <*(F . (d1,d9))*>
let p be FinSequence of D; ::_thesis: ( p = <*d1*> implies F [:] (p,d9) = <*(F . (d1,d9))*> )
assume A1: p = <*d1*> ; ::_thesis: F [:] (p,d9) = <*(F . (d1,d9))*>
A2: p . 1 = d1 by A1, FINSEQ_1:40;
reconsider r = F [:] (p,d9) as FinSequence of E by Th83;
len p = 1 by A1, FINSEQ_1:39;
then A3: len r = 1 by Th84;
then 1 in Seg (len r) ;
then 1 in dom r by FINSEQ_1:def_3;
then r . 1 = F . (d1,d9) by A2, FUNCOP_1:27;
hence F [:] (p,d9) = <*(F . (d1,d9))*> by A3, FINSEQ_1:40; ::_thesis: verum
end;
theorem :: FINSEQ_2:87
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))*>
proof
let D, D9, E be non empty set ; ::_thesis: 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))*>
let d1, d2 be Element of D; ::_thesis: 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))*>
let d9 be Element of D9; ::_thesis: 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))*>
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D st p = <*d1,d2*> holds
F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9))*>
let p be FinSequence of D; ::_thesis: ( p = <*d1,d2*> implies F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9))*> )
assume A1: p = <*d1,d2*> ; ::_thesis: F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9))*>
A2: p . 2 = d2 by A1, FINSEQ_1:44;
reconsider r = F [:] (p,d9) as FinSequence of E by Th83;
len p = 2 by A1, FINSEQ_1:44;
then A3: len r = 2 by Th84;
then 2 in Seg (len r) ;
then 2 in dom r by FINSEQ_1:def_3;
then A4: r . 2 = F . (d2,d9) by A2, FUNCOP_1:27;
1 in Seg (len r) by A3;
then A5: 1 in dom r by FINSEQ_1:def_3;
p . 1 = d1 by A1, FINSEQ_1:44;
then r . 1 = F . (d1,d9) by A5, FUNCOP_1:27;
hence F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9))*> by A3, A4, FINSEQ_1:44; ::_thesis: verum
end;
theorem :: FINSEQ_2:88
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))*>
proof
let D, D9, E be non empty set ; ::_thesis: 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))*>
let d1, d2, d3 be Element of D; ::_thesis: 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))*>
let d9 be Element of D9; ::_thesis: 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))*>
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D st p = <*d1,d2,d3*> holds
F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9)),(F . (d3,d9))*>
let p be FinSequence of D; ::_thesis: ( p = <*d1,d2,d3*> implies F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9)),(F . (d3,d9))*> )
assume A1: p = <*d1,d2,d3*> ; ::_thesis: F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9)),(F . (d3,d9))*>
A2: p . 2 = d2 by A1, FINSEQ_1:45;
reconsider r = F [:] (p,d9) as FinSequence of E by Th83;
len p = 3 by A1, FINSEQ_1:45;
then A3: len r = 3 by Th84;
then 2 in Seg (len r) ;
then 2 in dom r by FINSEQ_1:def_3;
then A4: r . 2 = F . (d2,d9) by A2, FUNCOP_1:27;
A5: p . 3 = d3 by A1, FINSEQ_1:45;
A6: p . 1 = d1 by A1, FINSEQ_1:45;
3 in Seg (len r) by A3;
then 3 in dom r by FINSEQ_1:def_3;
then A7: r . 3 = F . (d3,d9) by A5, FUNCOP_1:27;
1 in Seg (len r) by A3;
then 1 in dom r by FINSEQ_1:def_3;
then r . 1 = F . (d1,d9) by A6, FUNCOP_1:27;
hence F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9)),(F . (d3,d9))*> by A3, A4, A7, FINSEQ_1:45; ::_thesis: verum
end;
definition
let D be set ;
mode FinSequenceSet of D -> set means :Def3: :: FINSEQ_2:def 3
for a being set st a in it holds
a is FinSequence of D;
existence
ex b1 being set st
for a being set st a in b1 holds
a is FinSequence of D
proof
take D * ; ::_thesis: for a being set st a in D * holds
a is FinSequence of D
thus for a being set st a in D * holds
a is FinSequence of D by FINSEQ_1:def_11; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines FinSequenceSet FINSEQ_2:def_3_:_
for D, b2 being set holds
( b2 is FinSequenceSet of D iff for a being set st a in b2 holds
a is FinSequence of D );
definition
let D be set ;
let S be FinSequenceSet of D;
:: original: Element
redefine mode Element of S -> FinSequence of D;
coherence
for b1 being Element of S holds b1 is FinSequence of D
proof
percases ( not S is empty or S is empty ) ;
suppose not S is empty ; ::_thesis: for b1 being Element of S holds b1 is FinSequence of D
hence for b1 being Element of S holds b1 is FinSequence of D by Def3; ::_thesis: verum
end;
suppose S is empty ; ::_thesis: for b1 being Element of S holds b1 is FinSequence of D
then S = <*> D ;
hence for b1 being Element of S holds b1 is FinSequence of D by SUBSET_1:def_1; ::_thesis: verum
end;
end;
end;
end;
registration
let D be set ;
cluster non empty for FinSequenceSet of D;
existence
not for b1 being FinSequenceSet of D holds b1 is empty
proof
{(<*> D)} is FinSequenceSet of D
proof
let a be set ; :: according to FINSEQ_2:def_3 ::_thesis: ( a in {(<*> D)} implies a is FinSequence of D )
thus ( a in {(<*> D)} implies a is FinSequence of D ) by TARSKI:def_1; ::_thesis: verum
end;
hence not for b1 being FinSequenceSet of D holds b1 is empty ; ::_thesis: verum
end;
end;
theorem Th89: :: FINSEQ_2:89
for D being set holds D * is FinSequenceSet of D
proof
let D be set ; ::_thesis: D * is FinSequenceSet of D
D * is FinSequenceSet of D
proof
let a be set ; :: according to FINSEQ_2:def_3 ::_thesis: ( a in D * implies a is FinSequence of D )
thus ( a in D * implies a is FinSequence of D ) by FINSEQ_1:def_11; ::_thesis: verum
end;
hence D * is FinSequenceSet of D ; ::_thesis: verum
end;
definition
let D be set ;
:: original: *
redefine funcD * -> FinSequenceSet of D;
coherence
D * is FinSequenceSet of D by Th89;
end;
theorem :: FINSEQ_2:90
for D being set
for D9 being FinSequenceSet of D holds D9 c= D *
proof
let D be set ; ::_thesis: for D9 being FinSequenceSet of D holds D9 c= D *
let D9 be FinSequenceSet of D; ::_thesis: D9 c= D *
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in D9 or a in D * )
assume a in D9 ; ::_thesis: a in D *
then a is FinSequence of D by Def3;
hence a in D * by FINSEQ_1:def_11; ::_thesis: verum
end;
theorem :: FINSEQ_2:91
for D being non empty set
for D9 being Subset of D
for S being FinSequenceSet of D9 holds S is FinSequenceSet of D
proof
let D be non empty set ; ::_thesis: for D9 being Subset of D
for S being FinSequenceSet of D9 holds S is FinSequenceSet of D
let D9 be Subset of D; ::_thesis: for S being FinSequenceSet of D9 holds S is FinSequenceSet of D
let S be FinSequenceSet of D9; ::_thesis: S is FinSequenceSet of D
S is FinSequenceSet of D
proof
let a be set ; :: according to FINSEQ_2:def_3 ::_thesis: ( a in S implies a is FinSequence of D )
assume a in S ; ::_thesis: a is FinSequence of D
then reconsider p = a as FinSequence of D9 by Def3;
rng p c= D9 by FINSEQ_1:def_4;
then rng p c= D by XBOOLE_1:1;
hence a is FinSequence of D by FINSEQ_1:def_4; ::_thesis: verum
end;
hence S is FinSequenceSet of D ; ::_thesis: verum
end;
registration
let i be Nat;
let D be non empty set ;
cluster Relation-like NAT -defined D -valued Function-like V46() i -element FinSequence-like FinSubsequence-like countable for FinSequence of D;
existence
ex b1 being FinSequence of D st b1 is i -element
proof
take i |-> the Element of D ; ::_thesis: ( i |-> the Element of D is Element of bool [:NAT,D:] & i |-> the Element of D is FinSequence of D & i |-> the Element of D is i -element )
thus ( i |-> the Element of D is Element of bool [:NAT,D:] & i |-> the Element of D is FinSequence of D & i |-> the Element of D is i -element ) by Th63; ::_thesis: verum
end;
end;
definition
let i be Nat;
let D be non empty set ;
mode Tuple of i,D is i -element FinSequence of D;
end;
definition
let i be Nat;
let D be set ;
funci -tuples_on D -> FinSequenceSet of D equals :: FINSEQ_2:def 4
{ s where s is Element of D * : len s = i } ;
coherence
{ s where s is Element of D * : len s = i } is FinSequenceSet of D
proof
now__::_thesis:_for_a_being_set_st_a_in__{__s_where_s_is_Element_of_D_*_:_len_s_=_i__}__holds_
a_is_FinSequence_of_D
let a be set ; ::_thesis: ( a in { s where s is Element of D * : len s = i } implies a is FinSequence of D )
assume a in { s where s is Element of D * : len s = i } ; ::_thesis: a is FinSequence of D
then ex s being Element of D * st
( s = a & len s = i ) ;
hence a is FinSequence of D ; ::_thesis: verum
end;
hence { s where s is Element of D * : len s = i } is FinSequenceSet of D by Def3; ::_thesis: verum
end;
end;
:: deftheorem defines -tuples_on FINSEQ_2:def_4_:_
for i being Nat
for D being set holds i -tuples_on D = { s where s is Element of D * : len s = i } ;
registration
let i be Nat;
let D be non empty set ;
clusteri -tuples_on D -> non empty ;
coherence
not i -tuples_on D is empty
proof
set d = the Element of D;
i |-> the Element of D is FinSequence of D by Th63;
then reconsider S = i |-> the Element of D as Element of D * by FINSEQ_1:def_11;
len S = i by CARD_1:def_7;
then S in { s where s is Element of D * : len s = i } ;
hence not i -tuples_on D is empty ; ::_thesis: verum
end;
end;
registration
let D be non empty set ;
let i be Nat;
cluster -> i -element for Element of i -tuples_on D;
coherence
for b1 being Element of i -tuples_on D holds b1 is i -element
proof
let z be Element of i -tuples_on D; ::_thesis: z is i -element
z in { p9 where p9 is Element of D * : len p9 = i } ;
then ex p9 being Element of D * st
( p9 = z & len p9 = i ) ;
hence len z = i ; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;
theorem Th92: :: FINSEQ_2:92
for D being set
for z being FinSequence of D holds z is Element of (len z) -tuples_on D
proof
let D be set ; ::_thesis: for z being FinSequence of D holds z is Element of (len z) -tuples_on D
let z be FinSequence of D; ::_thesis: z is Element of (len z) -tuples_on D
z is Element of D * by FINSEQ_1:def_11;
then z in { z9 where z9 is Element of D * : len z9 = len z } ;
hence z is Element of (len z) -tuples_on D ; ::_thesis: verum
end;
theorem :: FINSEQ_2:93
for i being Nat
for D being set holds i -tuples_on D = Funcs ((Seg i),D)
proof
let i be Nat; ::_thesis: for D being set holds i -tuples_on D = Funcs ((Seg i),D)
let D be set ; ::_thesis: i -tuples_on D = Funcs ((Seg i),D)
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_i_-tuples_on_D_implies_z_in_Funcs_((Seg_i),D)_)_&_(_z_in_Funcs_((Seg_i),D)_implies_z_in_i_-tuples_on_D_)_)
reconsider j = i as Element of NAT by ORDINAL1:def_12;
let z be set ; ::_thesis: ( ( z in i -tuples_on D implies z in Funcs ((Seg i),D) ) & ( z in Funcs ((Seg i),D) implies z in i -tuples_on D ) )
thus ( z in i -tuples_on D implies z in Funcs ((Seg i),D) ) ::_thesis: ( z in Funcs ((Seg i),D) implies z in i -tuples_on D )
proof
assume z in i -tuples_on D ; ::_thesis: z in Funcs ((Seg i),D)
then consider s being Element of D * such that
A1: z = s and
A2: len s = i ;
A3: rng s c= D by FINSEQ_1:def_4;
dom s = Seg i by A2, FINSEQ_1:def_3;
hence z in Funcs ((Seg i),D) by A1, A3, FUNCT_2:def_2; ::_thesis: verum
end;
assume z in Funcs ((Seg i),D) ; ::_thesis: z in i -tuples_on D
then consider p being Function such that
A4: z = p and
A5: dom p = Seg j and
A6: rng p c= D by FUNCT_2:def_2;
p is FinSequence by A5, FINSEQ_1:def_2;
then p is FinSequence of D by A6, FINSEQ_1:def_4;
then reconsider p = p as Element of D * by FINSEQ_1:def_11;
len p = i by A5, FINSEQ_1:def_3;
hence z in i -tuples_on D by A4; ::_thesis: verum
end;
hence i -tuples_on D = Funcs ((Seg i),D) by TARSKI:1; ::_thesis: verum
end;
theorem :: FINSEQ_2:94
for D being set holds 0 -tuples_on D = {(<*> D)}
proof
let D be set ; ::_thesis: 0 -tuples_on D = {(<*> D)}
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_0_-tuples_on_D_implies_z_=_<*>_D_)_&_(_z_=_<*>_D_implies_z_in_0_-tuples_on_D_)_)
let z be set ; ::_thesis: ( ( z in 0 -tuples_on D implies z = <*> D ) & ( z = <*> D implies z in 0 -tuples_on D ) )
thus ( z in 0 -tuples_on D implies z = <*> D ) ::_thesis: ( z = <*> D implies z in 0 -tuples_on D )
proof
assume z in 0 -tuples_on D ; ::_thesis: z = <*> D
then ex s being Element of D * st
( z = s & len s = 0 ) ;
hence z = <*> D ; ::_thesis: verum
end;
( <*> D is Element of D * & len (<*> D) = 0 ) by FINSEQ_1:def_11;
hence ( z = <*> D implies z in 0 -tuples_on D ) ; ::_thesis: verum
end;
hence 0 -tuples_on D = {(<*> D)} by TARSKI:def_1; ::_thesis: verum
end;
theorem :: FINSEQ_2:95
for i being Nat
for D being non empty set
for z being Tuple of 0 ,D
for t being Tuple of i,D holds
( z ^ t = t & t ^ z = t ) by FINSEQ_1:34;
theorem Th96: :: FINSEQ_2:96
for D being non empty set holds 1 -tuples_on D = { <*d*> where d is Element of D : verum }
proof
let D be non empty set ; ::_thesis: 1 -tuples_on D = { <*d*> where d is Element of D : verum }
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_1_-tuples_on_D_implies_x_in__{__<*d*>_where_d_is_Element_of_D_:_verum__}__)_&_(_x_in__{__<*d*>_where_d_is_Element_of_D_:_verum__}__implies_x_in_1_-tuples_on_D_)_)
let x be set ; ::_thesis: ( ( x in 1 -tuples_on D implies x in { <*d*> where d is Element of D : verum } ) & ( x in { <*d*> where d is Element of D : verum } implies x in 1 -tuples_on D ) )
thus ( x in 1 -tuples_on D implies x in { <*d*> where d is Element of D : verum } ) ::_thesis: ( x in { <*d*> where d is Element of D : verum } implies x in 1 -tuples_on D )
proof
assume x in 1 -tuples_on D ; ::_thesis: x in { <*d*> where d is Element of D : verum }
then consider s being Element of D * such that
A1: x = s and
A2: len s = 1 ;
1 in Seg 1 ;
then 1 in dom s by A2, FINSEQ_1:def_3;
then reconsider d1 = s . 1 as Element of D by Th11;
s = <*d1*> by A2, FINSEQ_1:40;
hence x in { <*d*> where d is Element of D : verum } by A1; ::_thesis: verum
end;
assume x in { <*d*> where d is Element of D : verum } ; ::_thesis: x in 1 -tuples_on D
then consider d being Element of D such that
A3: x = <*d*> ;
( len <*d*> = 1 & <*d*> is Element of D * ) by FINSEQ_1:40, FINSEQ_1:def_11;
hence x in 1 -tuples_on D by A3; ::_thesis: verum
end;
hence 1 -tuples_on D = { <*d*> where d is Element of D : verum } by TARSKI:1; ::_thesis: verum
end;
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
proof
let i be Nat; ::_thesis: for D being non empty set
for z being Tuple of i,D holds z in i -tuples_on D
let D be non empty set ; ::_thesis: for z being Tuple of i,D holds z in i -tuples_on D
let z be Tuple of i,D; ::_thesis: z in i -tuples_on D
A1: z is Element of D * by FINSEQ_1:def_11;
len z = i by CARD_1:def_7;
hence z in i -tuples_on D by A1; ::_thesis: verum
end;
theorem Th97: :: FINSEQ_2:97
for D being non empty set
for z being Tuple of 1,D ex d being Element of D st z = <*d*>
proof
let D be non empty set ; ::_thesis: for z being Tuple of 1,D ex d being Element of D st z = <*d*>
let z be Tuple of 1,D; ::_thesis: ex d being Element of D st z = <*d*>
z in 1 -tuples_on D by Lm6;
then z in { <*d*> where d is Element of D : verum } by Th96;
hence ex d being Element of D st z = <*d*> ; ::_thesis: verum
end;
theorem Th98: :: FINSEQ_2:98
for D being non empty set
for d being Element of D holds <*d*> in 1 -tuples_on D
proof
let D be non empty set ; ::_thesis: for d being Element of D holds <*d*> in 1 -tuples_on D
let d be Element of D; ::_thesis: <*d*> in 1 -tuples_on D
<*d*> in { <*d1*> where d1 is Element of D : verum } ;
hence <*d*> in 1 -tuples_on D by Th96; ::_thesis: verum
end;
theorem Th99: :: FINSEQ_2:99
for D being non empty set holds 2 -tuples_on D = { <*d1,d2*> where d1, d2 is Element of D : verum }
proof
let D be non empty set ; ::_thesis: 2 -tuples_on D = { <*d1,d2*> where d1, d2 is Element of D : verum }
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_2_-tuples_on_D_implies_x_in__{__<*d1,d2*>_where_d1,_d2_is_Element_of_D_:_verum__}__)_&_(_x_in__{__<*d1,d2*>_where_d1,_d2_is_Element_of_D_:_verum__}__implies_x_in_2_-tuples_on_D_)_)
let x be set ; ::_thesis: ( ( x in 2 -tuples_on D implies x in { <*d1,d2*> where d1, d2 is Element of D : verum } ) & ( x in { <*d1,d2*> where d1, d2 is Element of D : verum } implies x in 2 -tuples_on D ) )
thus ( x in 2 -tuples_on D implies x in { <*d1,d2*> where d1, d2 is Element of D : verum } ) ::_thesis: ( x in { <*d1,d2*> where d1, d2 is Element of D : verum } implies x in 2 -tuples_on D )
proof
assume x in 2 -tuples_on D ; ::_thesis: x in { <*d1,d2*> where d1, d2 is Element of D : verum }
then consider s being Element of D * such that
A1: x = s and
A2: len s = 2 ;
2 in Seg 2 ;
then A3: 2 in dom s by A2, FINSEQ_1:def_3;
1 in Seg 2 ;
then 1 in dom s by A2, FINSEQ_1:def_3;
then reconsider d19 = s . 1, d29 = s . 2 as Element of D by A3, Th11;
s = <*d19,d29*> by A2, FINSEQ_1:44;
hence x in { <*d1,d2*> where d1, d2 is Element of D : verum } by A1; ::_thesis: verum
end;
assume x in { <*d1,d2*> where d1, d2 is Element of D : verum } ; ::_thesis: x in 2 -tuples_on D
then consider d1, d2 being Element of D such that
A4: x = <*d1,d2*> ;
<*d1,d2*> is FinSequence of D by Th13;
then ( len <*d1,d2*> = 2 & <*d1,d2*> is Element of D * ) by FINSEQ_1:44, FINSEQ_1:def_11;
hence x in 2 -tuples_on D by A4; ::_thesis: verum
end;
hence 2 -tuples_on D = { <*d1,d2*> where d1, d2 is Element of D : verum } by TARSKI:1; ::_thesis: verum
end;
theorem :: FINSEQ_2:100
for D being non empty set
for z being Tuple of 2,D ex d1, d2 being Element of D st z = <*d1,d2*>
proof
let D be non empty set ; ::_thesis: for z being Tuple of 2,D ex d1, d2 being Element of D st z = <*d1,d2*>
let z be Tuple of 2,D; ::_thesis: ex d1, d2 being Element of D st z = <*d1,d2*>
A1: z is Element of D * by FINSEQ_1:def_11;
len z = 2 by CARD_1:def_7;
then z in 2 -tuples_on D by A1;
then z in { <*d1,d2*> where d1, d2 is Element of D : verum } by Th99;
hence ex d1, d2 being Element of D st z = <*d1,d2*> ; ::_thesis: verum
end;
theorem Th101: :: FINSEQ_2:101
for D being non empty set
for d1, d2 being Element of D holds <*d1,d2*> in 2 -tuples_on D
proof
let D be non empty set ; ::_thesis: for d1, d2 being Element of D holds <*d1,d2*> in 2 -tuples_on D
let d1, d2 be Element of D; ::_thesis: <*d1,d2*> in 2 -tuples_on D
<*d1,d2*> in { <*c1,c2*> where c1, c2 is Element of D : verum } ;
hence <*d1,d2*> in 2 -tuples_on D by Th99; ::_thesis: verum
end;
theorem Th102: :: FINSEQ_2:102
for D being non empty set holds 3 -tuples_on D = { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum }
proof
let D be non empty set ; ::_thesis: 3 -tuples_on D = { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum }
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_3_-tuples_on_D_implies_x_in__{__<*d1,d2,d3*>_where_d1,_d2,_d3_is_Element_of_D_:_verum__}__)_&_(_x_in__{__<*d1,d2,d3*>_where_d1,_d2,_d3_is_Element_of_D_:_verum__}__implies_x_in_3_-tuples_on_D_)_)
let x be set ; ::_thesis: ( ( x in 3 -tuples_on D implies x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } ) & ( x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } implies x in 3 -tuples_on D ) )
thus ( x in 3 -tuples_on D implies x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } ) ::_thesis: ( x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } implies x in 3 -tuples_on D )
proof
assume x in 3 -tuples_on D ; ::_thesis: x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum }
then consider s being Element of D * such that
A1: x = s and
A2: len s = 3 ;
2 in Seg 3 ;
then A3: 2 in dom s by A2, FINSEQ_1:def_3;
3 in Seg 3 ;
then A4: 3 in dom s by A2, FINSEQ_1:def_3;
1 in Seg 3 ;
then 1 in dom s by A2, FINSEQ_1:def_3;
then reconsider d19 = s . 1, d29 = s . 2, d39 = s . 3 as Element of D by A3, A4, Th11;
s = <*d19,d29,d39*> by A2, FINSEQ_1:45;
hence x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } by A1; ::_thesis: verum
end;
assume x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } ; ::_thesis: x in 3 -tuples_on D
then consider d1, d2, d3 being Element of D such that
A5: x = <*d1,d2,d3*> ;
<*d1,d2,d3*> is FinSequence of D by Th14;
then ( len <*d1,d2,d3*> = 3 & <*d1,d2,d3*> is Element of D * ) by FINSEQ_1:45, FINSEQ_1:def_11;
hence x in 3 -tuples_on D by A5; ::_thesis: verum
end;
hence 3 -tuples_on D = { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } by TARSKI:1; ::_thesis: verum
end;
theorem :: FINSEQ_2:103
for D being non empty set
for z being Tuple of 3,D ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*>
proof
let D be non empty set ; ::_thesis: for z being Tuple of 3,D ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*>
let z be Tuple of 3,D; ::_thesis: ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*>
A1: z is Element of D * by FINSEQ_1:def_11;
len z = 3 by CARD_1:def_7;
then z in 3 -tuples_on D by A1;
then z in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } by Th102;
hence ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*> ; ::_thesis: verum
end;
theorem Th104: :: FINSEQ_2:104
for D being non empty set
for d1, d2, d3 being Element of D holds <*d1,d2,d3*> in 3 -tuples_on D
proof
let D be non empty set ; ::_thesis: for d1, d2, d3 being Element of D holds <*d1,d2,d3*> in 3 -tuples_on D
let d1, d2, d3 be Element of D; ::_thesis: <*d1,d2,d3*> in 3 -tuples_on D
<*d1,d2,d3*> in { <*c1,c2,c3*> where c1, c2, c3 is Element of D : verum } ;
hence <*d1,d2,d3*> in 3 -tuples_on D by Th102; ::_thesis: verum
end;
theorem Th105: :: FINSEQ_2:105
for i, j being Nat
for D being non empty set holds (i + j) -tuples_on D = { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }
proof
let i, j be Nat; ::_thesis: for D being non empty set holds (i + j) -tuples_on D = { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }
let D be non empty set ; ::_thesis: (i + j) -tuples_on D = { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }
set T = { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(i_+_j)_-tuples_on_D_implies_x_in__{__(z_^_t)_where_z_is_Tuple_of_i,D,_t_is_Tuple_of_j,D_:_verum__}__)_&_(_x_in__{__(z_^_t)_where_z_is_Tuple_of_i,D,_t_is_Tuple_of_j,D_:_verum__}__implies_x_in_(i_+_j)_-tuples_on_D_)_)
let x be set ; ::_thesis: ( ( x in (i + j) -tuples_on D implies x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } ) & ( x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } implies x in (i + j) -tuples_on D ) )
thus ( x in (i + j) -tuples_on D implies x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } ) ::_thesis: ( x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } implies x in (i + j) -tuples_on D )
proof
assume x in (i + j) -tuples_on D ; ::_thesis: x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }
then consider s being Element of D * such that
A1: x = s and
A2: len s = i + j ;
consider z, t being FinSequence of D such that
A3: ( len z = i & len t = j ) and
A4: s = z ^ t by A2, Th23;
( z is Tuple of i,D & t is Tuple of j,D ) by A3, CARD_1:def_7;
hence x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } by A1, A4; ::_thesis: verum
end;
assume x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } ; ::_thesis: x in (i + j) -tuples_on D
then consider z being Tuple of i,D, t being Tuple of j,D such that
A5: x = z ^ t ;
( len z = i & len t = j ) by CARD_1:def_7;
then A6: len (z ^ t) = i + j by FINSEQ_1:22;
z ^ t is Element of D * by FINSEQ_1:def_11;
hence x in (i + j) -tuples_on D by A5, A6; ::_thesis: verum
end;
hence (i + j) -tuples_on D = { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } by TARSKI:1; ::_thesis: verum
end;
theorem Th106: :: FINSEQ_2:106
for i, j being Nat
for D being non empty set
for s being Tuple of i + j,D ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t
proof
let i, j be Nat; ::_thesis: for D being non empty set
for s being Tuple of i + j,D ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t
let D be non empty set ; ::_thesis: for s being Tuple of i + j,D ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t
let s be Tuple of i + j,D; ::_thesis: ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t
A1: s is Element of D * by FINSEQ_1:def_11;
len s = i + j by CARD_1:def_7;
then s in (i + j) -tuples_on D by A1;
then s in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } by Th105;
then consider z being Tuple of i,D, t being Tuple of j,D such that
A2: s = z ^ t ;
reconsider z = z as Element of i -tuples_on D by Lm6;
reconsider t = t as Element of j -tuples_on D by Lm6;
s = z ^ t by A2;
hence ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t ; ::_thesis: verum
end;
theorem :: FINSEQ_2:107
for i, j being Nat
for D being non empty set
for z being Tuple of i,D
for t being Tuple of j,D holds z ^ t is Tuple of i + j,D
proof
let i, j be Nat; ::_thesis: for D being non empty set
for z being Tuple of i,D
for t being Tuple of j,D holds z ^ t is Tuple of i + j,D
let D be non empty set ; ::_thesis: for z being Tuple of i,D
for t being Tuple of j,D holds z ^ t is Tuple of i + j,D
let z be Tuple of i,D; ::_thesis: for t being Tuple of j,D holds z ^ t is Tuple of i + j,D
let t be Tuple of j,D; ::_thesis: z ^ t is Tuple of i + j,D
z ^ t in { (z9 ^ t9) where z9 is Tuple of i,D, t9 is Tuple of j,D : verum } ;
then z ^ t in (i + j) -tuples_on D by Th105;
hence z ^ t is Tuple of i + j,D ; ::_thesis: verum
end;
theorem :: FINSEQ_2:108
for D being non empty set holds D * = union { (i -tuples_on D) where i is Element of NAT : verum }
proof
let D be non empty set ; ::_thesis: D * = union { (i -tuples_on D) where i is Element of NAT : verum }
for a being set holds
( a in D * iff a in union { (i -tuples_on D) where i is Element of NAT : verum } )
proof
let a be set ; ::_thesis: ( a in D * iff a in union { (i -tuples_on D) where i is Element of NAT : verum } )
thus ( a in D * implies a in union { (i -tuples_on D) where i is Element of NAT : verum } ) ::_thesis: ( a in union { (i -tuples_on D) where i is Element of NAT : verum } implies a in D * )
proof
assume a in D * ; ::_thesis: a in union { (i -tuples_on D) where i is Element of NAT : verum }
then reconsider a = a as FinSequence of D by FINSEQ_1:def_11;
( a is Element of (len a) -tuples_on D & (len a) -tuples_on D in { (i -tuples_on D) where i is Element of NAT : verum } ) by Th92;
hence a in union { (i -tuples_on D) where i is Element of NAT : verum } by TARSKI:def_4; ::_thesis: verum
end;
assume a in union { (i -tuples_on D) where i is Element of NAT : verum } ; ::_thesis: a in D *
then consider Z being set such that
A1: a in Z and
A2: Z in { (i -tuples_on D) where i is Element of NAT : verum } by TARSKI:def_4;
consider i being Element of NAT such that
A3: Z = i -tuples_on D by A2;
ex s being Element of D * st
( s = a & len s = i ) by A1, A3;
hence a in D * ; ::_thesis: verum
end;
hence D * = union { (i -tuples_on D) where i is Element of NAT : verum } by TARSKI:1; ::_thesis: verum
end;
theorem :: FINSEQ_2:109
for i being Nat
for D being non empty set
for D9 being non empty Subset of D
for z being Tuple of i,D9 holds z is Element of i -tuples_on D
proof
let i be Nat; ::_thesis: for D being non empty set
for D9 being non empty Subset of D
for z being Tuple of i,D9 holds z is Element of i -tuples_on D
let D be non empty set ; ::_thesis: for D9 being non empty Subset of D
for z being Tuple of i,D9 holds z is Element of i -tuples_on D
let D9 be non empty Subset of D; ::_thesis: for z being Tuple of i,D9 holds z is Element of i -tuples_on D
let z be Tuple of i,D9; ::_thesis: z is Element of i -tuples_on D
z is Tuple of i,D by Th24;
hence z is Element of i -tuples_on D by Lm6; ::_thesis: verum
end;
Lm7: for i being Nat
for x, A being set st x in i -tuples_on A holds
x is b1 -element FinSequence
proof
let i be Nat; ::_thesis: for x, A being set st x in i -tuples_on A holds
x is i -element FinSequence
let x, A be set ; ::_thesis: ( x in i -tuples_on A implies x is i -element FinSequence )
assume x in i -tuples_on A ; ::_thesis: x is i -element FinSequence
then x in { s where s is Element of A * : len s = i } ;
then ex s being Element of A * st
( x = s & len s = i ) ;
hence x is i -element FinSequence by CARD_1:def_7; ::_thesis: verum
end;
theorem :: FINSEQ_2:110
for i, j being Nat
for A being set
for D being non empty set st i -tuples_on D = j -tuples_on A holds
i = j
proof
let i, j be Nat; ::_thesis: for A being set
for D being non empty set st i -tuples_on D = j -tuples_on A holds
i = j
let A be set ; ::_thesis: for D being non empty set st i -tuples_on D = j -tuples_on A holds
i = j
let D be non empty set ; ::_thesis: ( i -tuples_on D = j -tuples_on A implies i = j )
set f = i |-> the Element of D;
i |-> the Element of D is Tuple of i,D by Th63;
then A1: i |-> the Element of D in i -tuples_on D by Lm6;
assume i -tuples_on D = j -tuples_on A ; ::_thesis: i = j
then i |-> the Element of D in j -tuples_on A by A1;
then i |-> the Element of D is j -element by Lm7;
then len (i |-> the Element of D) = j by CARD_1:def_7;
hence i = j by CARD_1:def_7; ::_thesis: verum
end;
theorem :: FINSEQ_2:111
for i being Nat holds idseq i is Element of i -tuples_on NAT
proof
let i be Nat; ::_thesis: idseq i is Element of i -tuples_on NAT
( idseq i is FinSequence of NAT & len (idseq i) = i ) by Th48, CARD_1:def_7;
hence idseq i is Element of i -tuples_on NAT by Th92; ::_thesis: verum
end;
theorem Th112: :: FINSEQ_2:112
for i being Nat
for D being non empty set
for d being Element of D holds i |-> d is Element of i -tuples_on D
proof
let i be Nat; ::_thesis: for D being non empty set
for d being Element of D holds i |-> d is Element of i -tuples_on D
let D be non empty set ; ::_thesis: for d being Element of D holds i |-> d is Element of i -tuples_on D
let d be Element of D; ::_thesis: i |-> d is Element of i -tuples_on D
( i |-> d is FinSequence of D & len (i |-> d) = i ) by Th63, CARD_1:def_7;
hence i |-> d is Element of i -tuples_on D by Lm6; ::_thesis: verum
end;
theorem :: FINSEQ_2:113
for i being Nat
for D, D9 being non empty set
for z being Tuple of i,D
for f being Function of D,D9 holds f * z is Element of i -tuples_on D9
proof
let i be Nat; ::_thesis: for D, D9 being non empty set
for z being Tuple of i,D
for f being Function of D,D9 holds f * z is Element of i -tuples_on D9
let D, D9 be non empty set ; ::_thesis: for z being Tuple of i,D
for f being Function of D,D9 holds f * z is Element of i -tuples_on D9
let z be Tuple of i,D; ::_thesis: for f being Function of D,D9 holds f * z is Element of i -tuples_on D9
let f be Function of D,D9; ::_thesis: f * z is Element of i -tuples_on D9
reconsider s = f * z as FinSequence of D9 by Th32;
len z = i by CARD_1:def_7;
then len s = i by Th33;
hence f * z is Element of i -tuples_on D9 by Th92; ::_thesis: verum
end;
theorem Th114: :: FINSEQ_2:114
for i being Nat
for D being non empty set
for z being Tuple of i,D
for f being Function of (Seg i),(Seg i) st rng f = Seg i holds
z * f is Element of i -tuples_on D
proof
let i be Nat; ::_thesis: for D being non empty set
for z being Tuple of i,D
for f being Function of (Seg i),(Seg i) st rng f = Seg i holds
z * f is Element of i -tuples_on D
let D be non empty set ; ::_thesis: for z being Tuple of i,D
for f being Function of (Seg i),(Seg i) st rng f = Seg i holds
z * f is Element of i -tuples_on D
let z be Tuple of i,D; ::_thesis: for f being Function of (Seg i),(Seg i) st rng f = Seg i holds
z * f is Element of i -tuples_on D
let f be Function of (Seg i),(Seg i); ::_thesis: ( rng f = Seg i implies z * f is Element of i -tuples_on D )
A1: len z = i by CARD_1:def_7;
then A2: Seg i = dom z by FINSEQ_1:def_3;
then reconsider t = z * f as FinSequence of D by Th47;
assume rng f = Seg i ; ::_thesis: z * f is Element of i -tuples_on D
then len t = len z by A2, Th42;
hence z * f is Element of i -tuples_on D by A1, Th92; ::_thesis: verum
end;
theorem :: FINSEQ_2:115
for i being Nat
for D being non empty set
for z being Tuple of i,D
for f being Permutation of (Seg i) holds z * f is Tuple of i,D
proof
let i be Nat; ::_thesis: for D being non empty set
for z being Tuple of i,D
for f being Permutation of (Seg i) holds z * f is Tuple of i,D
let D be non empty set ; ::_thesis: for z being Tuple of i,D
for f being Permutation of (Seg i) holds z * f is Tuple of i,D
let z be Tuple of i,D; ::_thesis: for f being Permutation of (Seg i) holds z * f is Tuple of i,D
let f be Permutation of (Seg i); ::_thesis: z * f is Tuple of i,D
rng f = Seg i by FUNCT_2:def_3;
hence z * f is Tuple of i,D by Th114; ::_thesis: verum
end;
theorem :: FINSEQ_2:116
for i being Nat
for D being non empty set
for z being Tuple of i,D
for d being Element of D holds (z ^ <*d*>) . (i + 1) = d
proof
let i be Nat; ::_thesis: for D being non empty set
for z being Tuple of i,D
for d being Element of D holds (z ^ <*d*>) . (i + 1) = d
let D be non empty set ; ::_thesis: for z being Tuple of i,D
for d being Element of D holds (z ^ <*d*>) . (i + 1) = d
let z be Tuple of i,D; ::_thesis: for d being Element of D holds (z ^ <*d*>) . (i + 1) = d
let d be Element of D; ::_thesis: (z ^ <*d*>) . (i + 1) = d
len z = i by CARD_1:def_7;
hence (z ^ <*d*>) . (i + 1) = d by FINSEQ_1:42; ::_thesis: verum
end;
theorem :: FINSEQ_2:117
for i being Nat
for D being non empty set
for z being Tuple of i + 1,D ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>
proof
let i be Nat; ::_thesis: for D being non empty set
for z being Tuple of i + 1,D ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>
let D be non empty set ; ::_thesis: for z being Tuple of i + 1,D ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>
let z be Tuple of i + 1,D; ::_thesis: ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>
consider t being Element of i -tuples_on D, s being Element of 1 -tuples_on D such that
A1: z = t ^ s by Th106;
ex d being Element of D st s = <*d*> by Th97;
hence ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*> by A1; ::_thesis: verum
end;
theorem :: FINSEQ_2:118
for i being Nat
for D being non empty set
for z being Tuple of i,D holds z * (idseq i) = z
proof
let i be Nat; ::_thesis: for D being non empty set
for z being Tuple of i,D holds z * (idseq i) = z
let D be non empty set ; ::_thesis: for z being Tuple of i,D holds z * (idseq i) = z
let z be Tuple of i,D; ::_thesis: z * (idseq i) = z
len z = i by CARD_1:def_7;
hence z * (idseq i) = z by Th54; ::_thesis: verum
end;
theorem :: FINSEQ_2:119
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
proof
let i be Nat; ::_thesis: 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
let D be non empty set ; ::_thesis: 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
let z1, z2 be Tuple of i,D; ::_thesis: ( ( for j being Nat st j in Seg i holds
z1 . j = z2 . j ) implies z1 = z2 )
len z2 = i by CARD_1:def_7;
then A1: dom z2 = Seg i by FINSEQ_1:def_3;
len z1 = i by CARD_1:def_7;
then dom z1 = Seg i by FINSEQ_1:def_3;
hence ( ( for j being Nat st j in Seg i holds
z1 . j = z2 . j ) implies z1 = z2 ) by A1, FINSEQ_1:13; ::_thesis: verum
end;
theorem :: FINSEQ_2:120
for i being Nat
for D, D9, E being non empty set
for F being Function of [:D,D9:],E
for z1 being Tuple of i,D
for z2 being Tuple of i,D9 holds F .: (z1,z2) is Element of i -tuples_on E
proof
let i be Nat; ::_thesis: for D, D9, E being non empty set
for F being Function of [:D,D9:],E
for z1 being Tuple of i,D
for z2 being Tuple of i,D9 holds F .: (z1,z2) is Element of i -tuples_on E
let D, D9, E be non empty set ; ::_thesis: for F being Function of [:D,D9:],E
for z1 being Tuple of i,D
for z2 being Tuple of i,D9 holds F .: (z1,z2) is Element of i -tuples_on E
let F be Function of [:D,D9:],E; ::_thesis: for z1 being Tuple of i,D
for z2 being Tuple of i,D9 holds F .: (z1,z2) is Element of i -tuples_on E
let z1 be Tuple of i,D; ::_thesis: for z2 being Tuple of i,D9 holds F .: (z1,z2) is Element of i -tuples_on E
let z2 be Tuple of i,D9; ::_thesis: F .: (z1,z2) is Element of i -tuples_on E
reconsider r = F .: (z1,z2) as FinSequence of E by Th70;
( len z1 = i & len z2 = i ) by CARD_1:def_7;
then len r = i by Th72;
hence F .: (z1,z2) is Element of i -tuples_on E by Th92; ::_thesis: verum
end;
theorem :: FINSEQ_2:121
for i being Nat
for D, D9, E being non empty set
for d being Element of D
for F being Function of [:D,D9:],E
for z being Tuple of i,D9 holds F [;] (d,z) is Element of i -tuples_on E
proof
let i be Nat; ::_thesis: for D, D9, E being non empty set
for d being Element of D
for F being Function of [:D,D9:],E
for z being Tuple of i,D9 holds F [;] (d,z) is Element of i -tuples_on E
let D, D9, E be non empty set ; ::_thesis: for d being Element of D
for F being Function of [:D,D9:],E
for z being Tuple of i,D9 holds F [;] (d,z) is Element of i -tuples_on E
let d be Element of D; ::_thesis: for F being Function of [:D,D9:],E
for z being Tuple of i,D9 holds F [;] (d,z) is Element of i -tuples_on E
let F be Function of [:D,D9:],E; ::_thesis: for z being Tuple of i,D9 holds F [;] (d,z) is Element of i -tuples_on E
let z be Tuple of i,D9; ::_thesis: F [;] (d,z) is Element of i -tuples_on E
reconsider r = F [;] (d,z) as FinSequence of E by Th77;
len z = i by CARD_1:def_7;
then len r = i by Th78;
hence F [;] (d,z) is Element of i -tuples_on E by Th92; ::_thesis: verum
end;
theorem :: FINSEQ_2:122
for i being Nat
for D, D9, E being non empty set
for d9 being Element of D9
for F being Function of [:D,D9:],E
for z being Tuple of i,D holds F [:] (z,d9) is Element of i -tuples_on E
proof
let i be Nat; ::_thesis: for D, D9, E being non empty set
for d9 being Element of D9
for F being Function of [:D,D9:],E
for z being Tuple of i,D holds F [:] (z,d9) is Element of i -tuples_on E
let D, D9, E be non empty set ; ::_thesis: for d9 being Element of D9
for F being Function of [:D,D9:],E
for z being Tuple of i,D holds F [:] (z,d9) is Element of i -tuples_on E
let d9 be Element of D9; ::_thesis: for F being Function of [:D,D9:],E
for z being Tuple of i,D holds F [:] (z,d9) is Element of i -tuples_on E
let F be Function of [:D,D9:],E; ::_thesis: for z being Tuple of i,D holds F [:] (z,d9) is Element of i -tuples_on E
let z be Tuple of i,D; ::_thesis: F [:] (z,d9) is Element of i -tuples_on E
reconsider r = F [:] (z,d9) as FinSequence of E by Th83;
len z = i by CARD_1:def_7;
then len r = i by Th84;
hence F [:] (z,d9) is Element of i -tuples_on E by Th92; ::_thesis: verum
end;
theorem :: FINSEQ_2:123
for i, j being Nat
for x being set holds (i + j) |-> x = (i |-> x) ^ (j |-> x)
proof
let i, j be Nat; ::_thesis: for x being set holds (i + j) |-> x = (i |-> x) ^ (j |-> x)
let x be set ; ::_thesis: (i + j) |-> x = (i |-> x) ^ (j |-> x)
defpred S1[ Nat] means (i + $1) |-> x = (i |-> x) ^ ($1 |-> x);
A1: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A2: (i + j) |-> x = (i |-> x) ^ (j |-> x) ; ::_thesis: S1[j + 1]
thus (i + (j + 1)) |-> x = ((i + j) + 1) |-> x
.= ((i + j) |-> x) ^ <*x*> by Th60
.= (i |-> x) ^ ((j |-> x) ^ <*x*>) by A2, FINSEQ_1:32
.= (i |-> x) ^ ((j + 1) |-> x) by Th60 ; ::_thesis: verum
end;
(i + 0) |-> x = (i |-> x) ^ {} by FINSEQ_1:34
.= (i |-> x) ^ (0 |-> x) ;
then A3: S1[ 0 ] ;
for j being Nat holds S1[j] from NAT_1:sch_2(A3, A1);
hence (i + j) |-> x = (i |-> x) ^ (j |-> x) ; ::_thesis: verum
end;
theorem :: FINSEQ_2:124
for i being Nat
for D being non empty set
for x being Tuple of i,D holds dom x = Seg i
proof
let i be Nat; ::_thesis: for D being non empty set
for x being Tuple of i,D holds dom x = Seg i
let D be non empty set ; ::_thesis: for x being Tuple of i,D holds dom x = Seg i
let x be Tuple of i,D; ::_thesis: dom x = Seg i
len x = i by CARD_1:def_7;
hence dom x = Seg i by FINSEQ_1:def_3; ::_thesis: verum
end;
theorem :: FINSEQ_2:125
for f being Function
for x, y being set st x in dom f & y in dom f holds
f * <*x,y*> = <*(f . x),(f . y)*>
proof
let f be Function; ::_thesis: for x, y being set st x in dom f & y in dom f holds
f * <*x,y*> = <*(f . x),(f . y)*>
let x, y be set ; ::_thesis: ( x in dom f & y in dom f implies f * <*x,y*> = <*(f . x),(f . y)*> )
assume that
A1: x in dom f and
A2: y in dom f ; ::_thesis: f * <*x,y*> = <*(f . x),(f . y)*>
reconsider D = dom f, E = rng f as non empty set by A1, FUNCT_1:3;
rng <*x,y*> = {x,y} by Lm1;
then rng <*x,y*> c= D by A1, A2, ZFMISC_1:32;
then reconsider p = <*x,y*> as FinSequence of D by FINSEQ_1:def_4;
reconsider g = f as Function of D,E by FUNCT_2:def_1, RELSET_1:4;
thus f * <*x,y*> = g * p
.= <*(f . x),(f . y)*> by Th36 ; ::_thesis: verum
end;
theorem :: FINSEQ_2:126
for f being Function
for x, y, z being set st x in dom f & y in dom f & z in dom f holds
f * <*x,y,z*> = <*(f . x),(f . y),(f . z)*>
proof
let f be Function; ::_thesis: for x, y, z being set st x in dom f & y in dom f & z in dom f holds
f * <*x,y,z*> = <*(f . x),(f . y),(f . z)*>
let x, y, z be set ; ::_thesis: ( x in dom f & y in dom f & z in dom f implies f * <*x,y,z*> = <*(f . x),(f . y),(f . z)*> )
assume that
A1: x in dom f and
A2: ( y in dom f & z in dom f ) ; ::_thesis: f * <*x,y,z*> = <*(f . x),(f . y),(f . z)*>
reconsider D = dom f, E = rng f as non empty set by A1, FUNCT_1:3;
rng <*x,y,z*> = {x,y,z} by Lm2;
then A3: rng <*x,y,z*> = {x,y} \/ {z} by ENUMSET1:3;
( {x,y} c= D & {z} c= D ) by A1, A2, ZFMISC_1:31, ZFMISC_1:32;
then rng <*x,y,z*> c= D by A3, XBOOLE_1:8;
then reconsider p = <*x,y,z*> as FinSequence of D by FINSEQ_1:def_4;
reconsider g = f as Function of D,E by FUNCT_2:def_1, RELSET_1:4;
thus f * <*x,y,z*> = g * p
.= <*(f . x),(f . y),(f . z)*> by Th37 ; ::_thesis: verum
end;
theorem :: FINSEQ_2:127
for x1, x2 being set holds rng <*x1,x2*> = {x1,x2} by Lm1;
theorem :: FINSEQ_2:128
for x1, x2, x3 being set holds rng <*x1,x2,x3*> = {x1,x2,x3} by Lm2;
begin
theorem :: FINSEQ_2:129
for p1, p2, q being FinSequence st p1 c= q & p2 c= q & len p1 = len p2 holds
p1 = p2
proof
let p1, p2, q be FinSequence; ::_thesis: ( p1 c= q & p2 c= q & len p1 = len p2 implies p1 = p2 )
assume that
A1: p1 c= q and
A2: p2 c= q and
A3: len p1 = len p2 ; ::_thesis: p1 = p2
reconsider i = len p1 as Element of NAT ;
A4: ( dom p1 = Seg i & dom p2 = Seg i ) by A3, FINSEQ_1:def_3;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_p1_holds_
p1_._j_=_p2_._j
let j be Nat; ::_thesis: ( j in dom p1 implies p1 . j = p2 . j )
assume A5: j in dom p1 ; ::_thesis: p1 . j = p2 . j
hence p1 . j = q . j by A1, GRFUNC_1:2
.= p2 . j by A2, A4, A5, GRFUNC_1:2 ;
::_thesis: verum
end;
hence p1 = p2 by A4, FINSEQ_1:13; ::_thesis: verum
end;
theorem :: FINSEQ_2:130
for D being non empty set
for s being FinSequence of D st s <> {} holds
ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w
proof
let D be non empty set ; ::_thesis: for s being FinSequence of D st s <> {} holds
ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w
let s be FinSequence of D; ::_thesis: ( s <> {} implies ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w )
defpred S1[ FinSequence of D] means ( $1 <> {} implies ex w being FinSequence of D ex n being Element of D st $1 = <*n*> ^ w );
A1: for s being FinSequence of D
for m being Element of D st S1[s] holds
S1[s ^ <*m*>]
proof
let s be FinSequence of D; ::_thesis: for m being Element of D st S1[s] holds
S1[s ^ <*m*>]
let m be Element of D; ::_thesis: ( S1[s] implies S1[s ^ <*m*>] )
assume A2: ( s <> {} implies ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w ) ; ::_thesis: S1[s ^ <*m*>]
assume s ^ <*m*> <> {} ; ::_thesis: ex w being FinSequence of D ex n being Element of D st s ^ <*m*> = <*n*> ^ w
percases ( s = {} or s <> {} ) ;
supposeA3: s = {} ; ::_thesis: ex w being FinSequence of D ex n being Element of D st s ^ <*m*> = <*n*> ^ w
reconsider w = <*> D as FinSequence of D ;
take w ; ::_thesis: ex n being Element of D st s ^ <*m*> = <*n*> ^ w
take n = m; ::_thesis: s ^ <*m*> = <*n*> ^ w
thus s ^ <*m*> = <*m*> by A3, FINSEQ_1:34
.= <*n*> ^ w by FINSEQ_1:34 ; ::_thesis: verum
end;
suppose s <> {} ; ::_thesis: ex w being FinSequence of D ex n being Element of D st s ^ <*m*> = <*n*> ^ w
then consider w being FinSequence of D, n being Element of D such that
A4: s = <*n*> ^ w by A2;
take w ^ <*m*> ; ::_thesis: ex n being Element of D st s ^ <*m*> = <*n*> ^ (w ^ <*m*>)
take n ; ::_thesis: s ^ <*m*> = <*n*> ^ (w ^ <*m*>)
thus s ^ <*m*> = <*n*> ^ (w ^ <*m*>) by A4, FINSEQ_1:32; ::_thesis: verum
end;
end;
end;
A5: S1[ <*> D] ;
for p being FinSequence of D holds S1[p] from FINSEQ_2:sch_2(A5, A1);
hence ( s <> {} implies ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w ) ; ::_thesis: verum
end;
registration
let D be set ;
cluster -> functional for FinSequenceSet of D;
coherence
for b1 being FinSequenceSet of D holds b1 is functional
proof
let f be FinSequenceSet of D; ::_thesis: f is functional
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in f or x is set )
thus ( not x in f or x is set ) by Def3; ::_thesis: verum
end;
end;
definition
let D be non empty set ;
let n be Nat;
let d be Element of D;
:: original: |->
redefine funcn |-> d -> Element of n -tuples_on D;
coherence
n |-> d is Element of n -tuples_on D by Th112;
end;
theorem :: FINSEQ_2:131
for i being Nat
for D being non empty set
for z being set holds
( z is Tuple of i,D iff z in i -tuples_on D )
proof
let i be Nat; ::_thesis: for D being non empty set
for z being set holds
( z is Tuple of i,D iff z in i -tuples_on D )
let D be non empty set ; ::_thesis: for z being set holds
( z is Tuple of i,D iff z in i -tuples_on D )
let z be set ; ::_thesis: ( z is Tuple of i,D iff z in i -tuples_on D )
thus ( z is Tuple of i,D implies z in i -tuples_on D ) by Lm6; ::_thesis: ( z in i -tuples_on D implies z is Tuple of i,D )
assume z in i -tuples_on D ; ::_thesis: z is Tuple of i,D
then ex s being Element of D * st
( z = s & len s = i ) ;
hence z is Tuple of i,D by CARD_1:def_7; ::_thesis: verum
end;
theorem Th132: :: FINSEQ_2:132
for A being set
for i being Element of NAT
for p being FinSequence holds
( p in i -tuples_on A iff ( len p = i & rng p c= A ) )
proof
let A be set ; ::_thesis: for i being Element of NAT
for p being FinSequence holds
( p in i -tuples_on A iff ( len p = i & rng p c= A ) )
let i be Element of NAT ; ::_thesis: for p being FinSequence holds
( p in i -tuples_on A iff ( len p = i & rng p c= A ) )
let p be FinSequence; ::_thesis: ( p in i -tuples_on A iff ( len p = i & rng p c= A ) )
hereby ::_thesis: ( len p = i & rng p c= A implies p in i -tuples_on A )
assume p in i -tuples_on A ; ::_thesis: ( len p = i & rng p c= A )
then ex q being Element of A * st
( p = q & len q = i ) ;
hence ( len p = i & rng p c= A ) by FINSEQ_1:def_4; ::_thesis: verum
end;
assume A1: len p = i ; ::_thesis: ( not rng p c= A or p in i -tuples_on A )
assume rng p c= A ; ::_thesis: p in i -tuples_on A
then p is FinSequence of A by FINSEQ_1:def_4;
then p in A * by FINSEQ_1:def_11;
hence p in i -tuples_on A by A1; ::_thesis: verum
end;
theorem :: FINSEQ_2:133
for A being set
for i being Element of NAT
for p being FinSequence of A holds
( p in i -tuples_on A iff len p = i )
proof
let A be set ; ::_thesis: for i being Element of NAT
for p being FinSequence of A holds
( p in i -tuples_on A iff len p = i )
let i be Element of NAT ; ::_thesis: for p being FinSequence of A holds
( p in i -tuples_on A iff len p = i )
let p be FinSequence of A; ::_thesis: ( p in i -tuples_on A iff len p = i )
rng p c= A by RELAT_1:def_19;
hence ( p in i -tuples_on A iff len p = i ) by Th132; ::_thesis: verum
end;
theorem :: FINSEQ_2:134
for A being set
for i being Element of NAT holds i -tuples_on A c= A *
proof
let A be set ; ::_thesis: for i being Element of NAT holds i -tuples_on A c= A *
let i be Element of NAT ; ::_thesis: i -tuples_on A c= A *
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in i -tuples_on A or x in A * )
assume x in i -tuples_on A ; ::_thesis: x in A *
then x is FinSequence of A by Def3;
hence x in A * by FINSEQ_1:def_11; ::_thesis: verum
end;
theorem Th135: :: FINSEQ_2:135
for A, x being set holds
( x in 1 -tuples_on A iff ex a being set st
( a in A & x = <*a*> ) )
proof
let A, x be set ; ::_thesis: ( x in 1 -tuples_on A iff ex a being set st
( a in A & x = <*a*> ) )
hereby ::_thesis: ( ex a being set st
( a in A & x = <*a*> ) implies x in 1 -tuples_on A )
assume x in 1 -tuples_on A ; ::_thesis: ex a being set st
( a in A & x = <*a*> )
then x in { s where s is Element of A * : len s = 1 } ;
then consider s being Element of A * such that
A1: x = s and
A2: len s = 1 ;
take a = s . 1; ::_thesis: ( a in A & x = <*a*> )
A3: ( rng <*a*> = {a} & a in {a} ) by FINSEQ_1:39, TARSKI:def_1;
A4: rng s c= A by RELAT_1:def_19;
x = <*a*> by A1, A2, FINSEQ_1:40;
hence ( a in A & x = <*a*> ) by A1, A3, A4; ::_thesis: verum
end;
given a being set such that A5: a in A and
A6: x = <*a*> ; ::_thesis: x in 1 -tuples_on A
reconsider A = A as non empty set by A5;
reconsider a = a as Element of A by A5;
<*a*> is Element of 1 -tuples_on A by Th98;
hence x in 1 -tuples_on A by A6; ::_thesis: verum
end;
theorem :: FINSEQ_2:136
for A, a being set st <*a*> in 1 -tuples_on A holds
a in A
proof
let A, a be set ; ::_thesis: ( <*a*> in 1 -tuples_on A implies a in A )
assume <*a*> in 1 -tuples_on A ; ::_thesis: a in A
then A1: ex a9 being set st
( a9 in A & <*a*> = <*a9*> ) by Th135;
<*a*> . 1 = a by FINSEQ_1:40;
hence a in A by A1, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th137: :: FINSEQ_2:137
for A, x being set holds
( x in 2 -tuples_on A iff ex a, b being set st
( a in A & b in A & x = <*a,b*> ) )
proof
let A, x be set ; ::_thesis: ( x in 2 -tuples_on A iff ex a, b being set st
( a in A & b in A & x = <*a,b*> ) )
hereby ::_thesis: ( ex a, b being set st
( a in A & b in A & x = <*a,b*> ) implies x in 2 -tuples_on A )
assume x in 2 -tuples_on A ; ::_thesis: ex a, b being set st
( a in A & b in A & x = <*a,b*> )
then x in { s where s is Element of A * : len s = 2 } ;
then consider s being Element of A * such that
A1: x = s and
A2: len s = 2 ;
take a = s . 1; ::_thesis: ex b being set st
( a in A & b in A & x = <*a,b*> )
take b = s . 2; ::_thesis: ( a in A & b in A & x = <*a,b*> )
A3: ( rng <*a,b*> = {a,b} & a in {a,b} ) by Lm1, TARSKI:def_2;
A4: ( b in {a,b} & rng s c= A ) by RELAT_1:def_19, TARSKI:def_2;
x = <*a,b*> by A1, A2, FINSEQ_1:44;
hence ( a in A & b in A & x = <*a,b*> ) by A1, A3, A4; ::_thesis: verum
end;
given a, b being set such that A5: a in A and
A6: b in A and
A7: x = <*a,b*> ; ::_thesis: x in 2 -tuples_on A
reconsider A = A as non empty set by A5;
reconsider a = a, b = b as Element of A by A5, A6;
<*a,b*> is Element of 2 -tuples_on A by Th101;
hence x in 2 -tuples_on A by A7; ::_thesis: verum
end;
theorem :: FINSEQ_2:138
for A, a, b being set st <*a,b*> in 2 -tuples_on A holds
( a in A & b in A )
proof
let A, a, b be set ; ::_thesis: ( <*a,b*> in 2 -tuples_on A implies ( a in A & b in A ) )
assume <*a,b*> in 2 -tuples_on A ; ::_thesis: ( a in A & b in A )
then A1: ex a9, b9 being set st
( a9 in A & b9 in A & <*a,b*> = <*a9,b9*> ) by Th137;
( <*a,b*> . 1 = a & <*a,b*> . 2 = b ) by FINSEQ_1:44;
hence ( a in A & b in A ) by A1, FINSEQ_1:44; ::_thesis: verum
end;
theorem Th139: :: FINSEQ_2:139
for A, x being set holds
( x in 3 -tuples_on A iff ex a, b, c being set st
( a in A & b in A & c in A & x = <*a,b,c*> ) )
proof
let A, x be set ; ::_thesis: ( x in 3 -tuples_on A iff ex a, b, c being set st
( a in A & b in A & c in A & x = <*a,b,c*> ) )
hereby ::_thesis: ( ex a, b, c being set st
( a in A & b in A & c in A & x = <*a,b,c*> ) implies x in 3 -tuples_on A )
assume x in 3 -tuples_on A ; ::_thesis: ex a, b, c being set st
( a in A & b in A & c in A & x = <*a,b,c*> )
then x in { s where s is Element of A * : len s = 3 } ;
then consider s being Element of A * such that
A1: x = s and
A2: len s = 3 ;
take a = s . 1; ::_thesis: ex b, c being set st
( a in A & b in A & c in A & x = <*a,b,c*> )
take b = s . 2; ::_thesis: ex c being set st
( a in A & b in A & c in A & x = <*a,b,c*> )
take c = s . 3; ::_thesis: ( a in A & b in A & c in A & x = <*a,b,c*> )
A3: ( rng <*a,b,c*> = {a,b,c} & a in {a,b,c} ) by Lm2, ENUMSET1:def_1;
A4: rng s c= A by RELAT_1:def_19;
A5: ( b in {a,b,c} & c in {a,b,c} ) by ENUMSET1:def_1;
x = <*a,b,c*> by A1, A2, FINSEQ_1:45;
hence ( a in A & b in A & c in A & x = <*a,b,c*> ) by A1, A3, A5, A4; ::_thesis: verum
end;
given a, b, c being set such that A6: a in A and
A7: ( b in A & c in A ) and
A8: x = <*a,b,c*> ; ::_thesis: x in 3 -tuples_on A
reconsider A = A as non empty set by A6;
reconsider a = a, b = b, c = c as Element of A by A6, A7;
<*a,b,c*> is Element of 3 -tuples_on A by Th104;
hence x in 3 -tuples_on A by A8; ::_thesis: verum
end;
theorem :: FINSEQ_2:140
for A, a, b, c being set st <*a,b,c*> in 3 -tuples_on A holds
( a in A & b in A & c in A )
proof
let A, a, b, c be set ; ::_thesis: ( <*a,b,c*> in 3 -tuples_on A implies ( a in A & b in A & c in A ) )
A1: <*a,b,c*> . 3 = c by FINSEQ_1:45;
assume <*a,b,c*> in 3 -tuples_on A ; ::_thesis: ( a in A & b in A & c in A )
then A2: ex a9, b9, c9 being set st
( a9 in A & b9 in A & c9 in A & <*a,b,c*> = <*a9,b9,c9*> ) by Th139;
( <*a,b,c*> . 1 = a & <*a,b,c*> . 2 = b ) by FINSEQ_1:45;
hence ( a in A & b in A & c in A ) by A2, A1, FINSEQ_1:45; ::_thesis: verum
end;
theorem :: FINSEQ_2:141
for i being Nat
for x, A being set st x in i -tuples_on A holds
x is b1 -element FinSequence by Lm7;
theorem :: FINSEQ_2:142
for A being non empty set
for n being Nat holds n -tuples_on A c= A *
proof
let A be non empty set ; ::_thesis: for n being Nat holds n -tuples_on A c= A *
let n be Nat; ::_thesis: n -tuples_on A c= A *
defpred S1[ Element of A * ] means len $1 = n;
{ s where s is Element of A * : S1[s] } c= A * from FRAENKEL:sch_10();
hence n -tuples_on A c= A * ; ::_thesis: verum
end;
theorem :: FINSEQ_2:143
for x being set
for n, m being Nat st n |-> x = m |-> x holds
n = m
proof
let x be set ; ::_thesis: for n, m being Nat st n |-> x = m |-> x holds
n = m
let n, m be Nat; ::_thesis: ( n |-> x = m |-> x implies n = m )
len (n |-> x) = n by CARD_1:def_7;
hence ( n |-> x = m |-> x implies n = m ) by CARD_1:def_7; ::_thesis: verum
end;
definition
let I be set ;
let M be ManySortedSet of I;
funcM # -> ManySortedSet of I * means :Def5: :: FINSEQ_2:def 5
for i being Element of I * holds it . i = product (M * i);
existence
ex b1 being ManySortedSet of I * st
for i being Element of I * holds b1 . i = product (M * i)
proof
defpred S1[ set , set ] means ex j being Element of I * st
( j = $1 & $2 = product (M * j) );
A1: for i being set st i in I * holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in I * implies ex j being set st S1[i,j] )
assume i in I * ; ::_thesis: ex j being set st S1[i,j]
then reconsider j = i as Element of I * ;
reconsider e = product (M * j) as set ;
take e ; ::_thesis: S1[i,e]
take j ; ::_thesis: ( j = i & e = product (M * j) )
thus ( j = i & e = product (M * j) ) ; ::_thesis: verum
end;
consider f being ManySortedSet of I * such that
A2: for i being set st i in I * holds
S1[i,f . i] from PBOOLE:sch_3(A1);
take f ; ::_thesis: for i being Element of I * holds f . i = product (M * i)
let i be Element of I * ; ::_thesis: f . i = product (M * i)
ex j being Element of I * st
( j = i & f . i = product (M * j) ) by A2;
hence f . i = product (M * i) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedSet of I * st ( for i being Element of I * holds b1 . i = product (M * i) ) & ( for i being Element of I * holds b2 . i = product (M * i) ) holds
b1 = b2
proof
let N1, N2 be ManySortedSet of I * ; ::_thesis: ( ( for i being Element of I * holds N1 . i = product (M * i) ) & ( for i being Element of I * holds N2 . i = product (M * i) ) implies N1 = N2 )
assume that
A3: for i being Element of I * holds N1 . i = product (M * i) and
A4: for i being Element of I * holds N2 . i = product (M * i) ; ::_thesis: N1 = N2
now__::_thesis:_for_i_being_set_st_i_in_I_*_holds_
N1_._i_=_N2_._i
let i be set ; ::_thesis: ( i in I * implies N1 . i = N2 . i )
assume i in I * ; ::_thesis: N1 . i = N2 . i
then reconsider e = i as Element of I * ;
thus N1 . i = product (M * e) by A3
.= N2 . i by A4 ; ::_thesis: verum
end;
hence N1 = N2 by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines # FINSEQ_2:def_5_:_
for I being set
for M being ManySortedSet of I
for b3 being ManySortedSet of I * holds
( b3 = M # iff for i being Element of I * holds b3 . i = product (M * i) );
registration
let I be set ;
let M be V2() ManySortedSet of I;
clusterM # -> V2() ;
coherence
M # is non-empty
proof
M # is V2()
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I * or not (M #) . i is empty )
assume i in I * ; ::_thesis: not (M #) . i is empty
then reconsider f = i as Element of I * ;
product (M * f) <> {} ;
hence not (M #) . i is empty by Def5; ::_thesis: verum
end;
hence M # is non-empty ; ::_thesis: verum
end;
end;
definition
let a be set ;
func *--> a -> Function of NAT,({a} *) means :Def6: :: FINSEQ_2:def 6
for n being Element of NAT holds it . n = n |-> a;
existence
ex b1 being Function of NAT,({a} *) st
for n being Element of NAT holds b1 . n = n |-> a
proof
defpred S1[ Element of NAT , set ] means $2 = $1 |-> a;
A1: for x being Element of NAT ex y being Element of {a} * st S1[x,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of {a} * st S1[n,y]
a is Element of {a} by TARSKI:def_1;
then n |-> a is FinSequence of {a} by Th63;
then reconsider u = n |-> a as Element of {a} * by FINSEQ_1:def_11;
take u ; ::_thesis: S1[n,u]
thus S1[n,u] ; ::_thesis: verum
end;
ex f being Function of NAT,({a} *) st
for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1);
hence ex b1 being Function of NAT,({a} *) st
for n being Element of NAT holds b1 . n = n |-> a ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of NAT,({a} *) st ( for n being Element of NAT holds b1 . n = n |-> a ) & ( for n being Element of NAT holds b2 . n = n |-> a ) holds
b1 = b2
proof
let f1, f2 be Function of NAT,({a} *); ::_thesis: ( ( for n being Element of NAT holds f1 . n = n |-> a ) & ( for n being Element of NAT holds f2 . n = n |-> a ) implies f1 = f2 )
assume that
A2: for n being Element of NAT holds f1 . n = n |-> a and
A3: for n being Element of NAT holds f2 . n = n |-> a ; ::_thesis: f1 = f2
now__::_thesis:_for_k_being_Element_of_NAT_holds_f1_._k_=_f2_._k
let k be Element of NAT ; ::_thesis: f1 . k = f2 . k
thus f1 . k = k |-> a by A2
.= f2 . k by A3 ; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines *--> FINSEQ_2:def_6_:_
for a being set
for b2 being Function of NAT,({a} *) holds
( b2 = *--> a iff for n being Element of NAT holds b2 . n = n |-> a );
theorem Th144: :: FINSEQ_2:144
for n being Element of NAT
for a, b being set holds (a .--> b) * (n |-> a) = n |-> b
proof
let n be Element of NAT ; ::_thesis: for a, b being set holds (a .--> b) * (n |-> a) = n |-> b
let a, b be set ; ::_thesis: (a .--> b) * (n |-> a) = n |-> b
A1: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_(n_|->_b)_implies_(_x_in_dom_(n_|->_a)_&_(n_|->_a)_._x_in_dom_(a_.-->_b)_)_)_&_(_x_in_dom_(n_|->_a)_&_(n_|->_a)_._x_in_dom_(a_.-->_b)_implies_x_in_dom_(n_|->_b)_)_)
let x be set ; ::_thesis: ( ( x in dom (n |-> b) implies ( x in dom (n |-> a) & (n |-> a) . x in dom (a .--> b) ) ) & ( x in dom (n |-> a) & (n |-> a) . x in dom (a .--> b) implies x in dom (n |-> b) ) )
hereby ::_thesis: ( x in dom (n |-> a) & (n |-> a) . x in dom (a .--> b) implies x in dom (n |-> b) )
assume x in dom (n |-> b) ; ::_thesis: ( x in dom (n |-> a) & (n |-> a) . x in dom (a .--> b) )
then A2: x in Seg n by FUNCOP_1:13;
hence x in dom (n |-> a) by FUNCOP_1:13; ::_thesis: (n |-> a) . x in dom (a .--> b)
( dom (a .--> b) = {a} & (n |-> a) . x = a ) by A2, FUNCOP_1:7, FUNCOP_1:13;
hence (n |-> a) . x in dom (a .--> b) by TARSKI:def_1; ::_thesis: verum
end;
assume that
A3: x in dom (n |-> a) and
(n |-> a) . x in dom (a .--> b) ; ::_thesis: x in dom (n |-> b)
x in Seg n by A3, FUNCOP_1:13;
hence x in dom (n |-> b) by FUNCOP_1:13; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_(n_|->_b)_holds_
(n_|->_b)_._x_=_(a_.-->_b)_._((n_|->_a)_._x)
let x be set ; ::_thesis: ( x in dom (n |-> b) implies (n |-> b) . x = (a .--> b) . ((n |-> a) . x) )
A4: a in {a} by TARSKI:def_1;
assume x in dom (n |-> b) ; ::_thesis: (n |-> b) . x = (a .--> b) . ((n |-> a) . x)
then A5: x in Seg n by FUNCOP_1:13;
hence (n |-> b) . x = b by FUNCOP_1:7
.= (a .--> b) . a by A4, FUNCOP_1:7
.= (a .--> b) . ((n |-> a) . x) by A5, FUNCOP_1:7 ;
::_thesis: verum
end;
hence (a .--> b) * (n |-> a) = n |-> b by A1, FUNCT_1:10; ::_thesis: verum
end;
theorem :: FINSEQ_2:145
for D being non empty set
for n being Element of NAT
for a being set
for M being ManySortedSet of {a} st M = a .--> D holds
((M #) * (*--> a)) . n = Funcs ((Seg n),D)
proof
let D be non empty set ; ::_thesis: for n being Element of NAT
for a being set
for M being ManySortedSet of {a} st M = a .--> D holds
((M #) * (*--> a)) . n = Funcs ((Seg n),D)
let n be Element of NAT ; ::_thesis: for a being set
for M being ManySortedSet of {a} st M = a .--> D holds
((M #) * (*--> a)) . n = Funcs ((Seg n),D)
let a be set ; ::_thesis: for M being ManySortedSet of {a} st M = a .--> D holds
((M #) * (*--> a)) . n = Funcs ((Seg n),D)
let M be ManySortedSet of {a}; ::_thesis: ( M = a .--> D implies ((M #) * (*--> a)) . n = Funcs ((Seg n),D) )
assume A1: M = a .--> D ; ::_thesis: ((M #) * (*--> a)) . n = Funcs ((Seg n),D)
a is Element of {a} by TARSKI:def_1;
then n |-> a is FinSequence of {a} by Th63;
then A2: n |-> a in {a} * by FINSEQ_1:def_11;
dom (*--> a) = NAT by FUNCT_2:def_1;
hence ((M #) * (*--> a)) . n = (M #) . ((*--> a) . n) by FUNCT_1:13
.= (M #) . (n |-> a) by Def6
.= product ((a .--> D) * (n |-> a)) by A1, A2, Def5
.= product (n |-> D) by Th144
.= Funcs ((Seg n),D) by CARD_3:11 ;
::_thesis: verum
end;
theorem :: FINSEQ_2:146
for F being NAT -defined total Function
for p being NAT -defined Function
for n being Element of NAT st Shift (p,n) c= F holds
for i being Element of NAT st i in dom p holds
F . (n + i) = p . i
proof
let F be NAT -defined total Function; ::_thesis: for p being NAT -defined Function
for n being Element of NAT st Shift (p,n) c= F holds
for i being Element of NAT st i in dom p holds
F . (n + i) = p . i
let p be NAT -defined Function; ::_thesis: for n being Element of NAT st Shift (p,n) c= F holds
for i being Element of NAT st i in dom p holds
F . (n + i) = p . i
let n be Element of NAT ; ::_thesis: ( Shift (p,n) c= F implies for i being Element of NAT st i in dom p holds
F . (n + i) = p . i )
assume A1: Shift (p,n) c= F ; ::_thesis: for i being Element of NAT st i in dom p holds
F . (n + i) = p . i
let i be Element of NAT ; ::_thesis: ( i in dom p implies F . (n + i) = p . i )
assume A2: i in dom p ; ::_thesis: F . (n + i) = p . i
then n + i in dom (Shift (p,n)) by VALUED_1:24;
hence F . (n + i) = (Shift (p,n)) . (n + i) by A1, GRFUNC_1:2
.= p . i by A2, VALUED_1:def_12 ;
::_thesis: verum
end;
registration
let i be Nat;
clusteri |-> 0 -> empty-yielding ;
coherence
i |-> 0 is empty-yielding
proof
let x be set ; :: according to FUNCT_1:def_8 ::_thesis: ( not x in dom (i |-> 0) or (i |-> 0) . x is empty )
dom (i |-> 0) = Seg i by FUNCOP_1:13;
hence ( not x in dom (i |-> 0) or (i |-> 0) . x is empty ) by Th57; ::_thesis: verum
end;
end;
registration
let D be set ;
cluster -> FinSequence-membered for FinSequenceSet of D;
coherence
for b1 being FinSequenceSet of D holds b1 is FinSequence-membered
proof
let A be FinSequenceSet of D; ::_thesis: A is FinSequence-membered
let x be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( not x in A or x is set )
thus ( not x in A or x is set ) by Def3; ::_thesis: verum
end;
end;