:: AFINSQ_1 semantic presentation
begin
theorem :: AFINSQ_1:1
for k, n being Nat st k = k /\ n holds
k <= n by NAT_1:46;
theorem Th2: :: AFINSQ_1:2
for n being Nat holds n \/ {n} = n + 1
proof
let n be Nat; ::_thesis: n \/ {n} = n + 1
n + 1 = succ n ;
hence n \/ {n} = n + 1 ; ::_thesis: verum
end;
theorem Th3: :: AFINSQ_1:3
for n being Nat holds Seg n c= n + 1
proof
let n be Nat; ::_thesis: Seg n c= n + 1
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg n or x in n + 1 )
assume A1: x in Seg n ; ::_thesis: x in n + 1
then reconsider x = x as Element of NAT ;
x <= n by A1, FINSEQ_1:1;
then x < n + 1 by NAT_1:13;
hence x in n + 1 by NAT_1:44; ::_thesis: verum
end;
theorem :: AFINSQ_1:4
for n being Nat holds n + 1 = {0} \/ (Seg n)
proof
let n be Nat; ::_thesis: n + 1 = {0} \/ (Seg n)
thus n + 1 c= {0} \/ (Seg n) :: according to XBOOLE_0:def_10 ::_thesis: {0} \/ (Seg n) c= n + 1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in n + 1 or x in {0} \/ (Seg n) )
assume x in n + 1 ; ::_thesis: x in {0} \/ (Seg n)
then x in { j where j is Element of NAT : j < n + 1 } by AXIOMS:4;
then consider j being Element of NAT such that
A1: j = x and
A2: j < n + 1 ;
( j = 0 or ( 1 < j + 1 & j <= n ) ) by A2, NAT_1:13, XREAL_1:29;
then ( j = 0 or ( 1 <= j & j <= n ) ) by NAT_1:13;
then ( x in {0} or x in Seg n ) by A1, FINSEQ_1:1, TARSKI:def_1;
hence x in {0} \/ (Seg n) by XBOOLE_0:def_3; ::_thesis: verum
end;
1 <= n + 1 by NAT_1:11;
then A3: {0} c= n + 1 by CARD_1:49, NAT_1:39;
Seg n c= n + 1 by Th3;
hence {0} \/ (Seg n) c= n + 1 by A3, XBOOLE_1:8; ::_thesis: verum
end;
theorem :: AFINSQ_1:5
for r being Function holds
( ( r is finite & r is T-Sequence-like ) iff ex n being Nat st dom r = n ) by FINSET_1:10, ORDINAL1:def_7;
definition
mode XFinSequence is finite T-Sequence;
end;
registration
let p be XFinSequence;
cluster dom p -> natural ;
coherence
dom p is natural ;
end;
notation
let p be XFinSequence;
synonym len p for card p;
end;
registration
let p be XFinSequence;
identify len p with dom p;
compatibility
len p = dom p
proof
thus len p = card (dom p) by CARD_1:62
.= dom p by CARD_1:def_2 ; ::_thesis: verum
end;
end;
definition
let p be XFinSequence;
:: original: len
redefine func len p -> Element of NAT ;
coherence
len p is Element of NAT
proof
card p = card p ;
hence len p is Element of NAT ; ::_thesis: verum
end;
end;
definition
let p be XFinSequence;
:: original: dom
redefine func dom p -> Subset of NAT;
coherence
dom p is Subset of NAT
proof
{ i where i is Element of NAT : i < len p } c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { i where i is Element of NAT : i < len p } or x in NAT )
assume x in { i where i is Element of NAT : i < len p } ; ::_thesis: x in NAT
then ex i being Element of NAT st
( i = x & i < len p ) ;
hence x in NAT ; ::_thesis: verum
end;
hence dom p is Subset of NAT by AXIOMS:4; ::_thesis: verum
end;
end;
theorem :: AFINSQ_1:6
for f being Function st ex k being Nat st dom f c= k holds
ex p being XFinSequence st f c= p
proof
let f be Function; ::_thesis: ( ex k being Nat st dom f c= k implies ex p being XFinSequence st f c= p )
given k being Nat such that A1: dom f c= k ; ::_thesis: ex p being XFinSequence st f c= p
deffunc H1( set ) -> set = f . $1;
consider g being Function such that
A2: ( dom g = k & ( for x being set st x in k holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
reconsider g = g as XFinSequence by A2, FINSET_1:10, ORDINAL1:def_7;
take g ; ::_thesis: f c= g
let y be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [y,b1] in f or [y,b1] in g )
let z be set ; ::_thesis: ( not [y,z] in f or [y,z] in g )
assume A3: [y,z] in f ; ::_thesis: [y,z] in g
then A4: y in dom f by XTUPLE_0:def_12;
then A5: [y,(g . y)] in g by A1, A2, FUNCT_1:1;
f . y = z by A3, A4, FUNCT_1:def_2;
hence [y,z] in g by A1, A2, A4, A5; ::_thesis: verum
end;
scheme :: AFINSQ_1:sch 1
XSeqEx{ F1() -> Nat, P1[ set , set ] } :
ex p being XFinSequence st
( dom p = F1() & ( for k being Nat st k in F1() holds
P1[k,p . k] ) )
provided
A1: for k being Nat st k in F1() holds
ex x being set st P1[k,x]
proof
A2: for x being set st x in F1() holds
ex y being set st P1[x,y]
proof
let x be set ; ::_thesis: ( x in F1() implies ex y being set st P1[x,y] )
assume A3: x in F1() ; ::_thesis: ex y being set st P1[x,y]
F1() = { i where i is Element of NAT : i < F1() } by AXIOMS:4;
then ex i being Element of NAT st
( i = x & i < F1() ) by A3;
hence ex y being set st P1[x,y] by A1, A3; ::_thesis: verum
end;
consider f being Function such that
A4: ( dom f = F1() & ( for x being set st x in F1() holds
P1[x,f . x] ) ) from CLASSES1:sch_1(A2);
reconsider p = f as XFinSequence by A4, FINSET_1:10, ORDINAL1:def_7;
take p ; ::_thesis: ( dom p = F1() & ( for k being Nat st k in F1() holds
P1[k,p . k] ) )
thus ( dom p = F1() & ( for k being Nat st k in F1() holds
P1[k,p . k] ) ) by A4; ::_thesis: verum
end;
scheme :: AFINSQ_1:sch 2
XSeqLambda{ F1() -> Nat, F2( set ) -> set } :
ex p being XFinSequence st
( len p = F1() & ( for k being Nat st k in F1() holds
p . k = F2(k) ) )
proof
consider f being Function such that
A1: ( dom f = F1() & ( for x being set st x in F1() holds
f . x = F2(x) ) ) from FUNCT_1:sch_3();
reconsider p = f as XFinSequence by A1, FINSET_1:10, ORDINAL1:def_7;
take p ; ::_thesis: ( len p = F1() & ( for k being Nat st k in F1() holds
p . k = F2(k) ) )
thus ( len p = F1() & ( for k being Nat st k in F1() holds
p . k = F2(k) ) ) by A1; ::_thesis: verum
end;
theorem :: AFINSQ_1:7
for z being set
for p being XFinSequence st z in p holds
ex k being Nat st
( k in dom p & z = [k,(p . k)] )
proof
let z be set ; ::_thesis: for p being XFinSequence st z in p holds
ex k being Nat st
( k in dom p & z = [k,(p . k)] )
let p be XFinSequence; ::_thesis: ( z in p implies ex k being Nat st
( k in dom p & z = [k,(p . k)] ) )
assume A1: z in p ; ::_thesis: ex k being Nat st
( k in dom p & z = [k,(p . k)] )
then consider x, y being set such that
A2: z = [x,y] by RELAT_1:def_1;
x in dom p by A1, A2, FUNCT_1:1;
then reconsider k = x as Element of NAT ;
take k ; ::_thesis: ( k in dom p & z = [k,(p . k)] )
thus ( k in dom p & z = [k,(p . k)] ) by A1, A2, FUNCT_1:1; ::_thesis: verum
end;
theorem Th8: :: AFINSQ_1:8
for p, q being XFinSequence st dom p = dom q & ( for k being Nat st k in dom p holds
p . k = q . k ) holds
p = q
proof
let p, q be XFinSequence; ::_thesis: ( dom p = dom q & ( for k being Nat st k in dom p holds
p . k = q . k ) implies p = q )
assume that
A1: dom p = dom q and
A2: for k being Nat st k in dom p holds
p . k = q . k ; ::_thesis: p = q
for x being set st x in dom p holds
p . x = q . x by A2;
hence p = q by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th9: :: AFINSQ_1:9
for p, q being XFinSequence st len p = len q & ( for k being Nat st k < len p holds
p . k = q . k ) holds
p = q
proof
let p, q be XFinSequence; ::_thesis: ( len p = len q & ( for k being Nat st k < len p holds
p . k = q . k ) implies p = q )
assume that
A1: len p = len q and
A2: for k being Nat st k < len p holds
p . k = q . k ; ::_thesis: p = q
now__::_thesis:_for_x_being_set_st_x_in_dom_p_holds_
p_._x_=_q_._x
let x be set ; ::_thesis: ( x in dom p implies p . x = q . x )
assume A3: x in dom p ; ::_thesis: p . x = q . x
then reconsider k = x as Element of NAT ;
k < len p by A3, NAT_1:44;
hence p . x = q . x by A2; ::_thesis: verum
end;
hence p = q by A1, FUNCT_1:2; ::_thesis: verum
end;
registration
let p be XFinSequence;
let n be Nat;
clusterp | n -> finite ;
coherence
p | n is finite ;
end;
theorem :: AFINSQ_1:10
for f being Function
for p being XFinSequence st rng p c= dom f holds
f * p is XFinSequence
proof
let f be Function; ::_thesis: for p being XFinSequence st rng p c= dom f holds
f * p is XFinSequence
let p be XFinSequence; ::_thesis: ( rng p c= dom f implies f * p is XFinSequence )
assume rng p c= dom f ; ::_thesis: f * p is XFinSequence
then dom (f * p) = len p by RELAT_1:27;
hence f * p is XFinSequence by ORDINAL1:def_7; ::_thesis: verum
end;
theorem Th11: :: AFINSQ_1:11
for k being Nat
for p being XFinSequence st k < len p holds
dom (p | k) = k
proof
let k be Nat; ::_thesis: for p being XFinSequence st k < len p holds
dom (p | k) = k
let p be XFinSequence; ::_thesis: ( k < len p implies dom (p | k) = k )
assume k < len p ; ::_thesis: dom (p | k) = k
then k c= len p by NAT_1:39;
hence dom (p | k) = k by RELAT_1:62; ::_thesis: verum
end;
registration
let D be set ;
cluster Relation-like D -valued T-Sequence-like Function-like finite for set ;
existence
ex b1 being T-Sequence of D st b1 is finite
proof
{} is T-Sequence of D by ORDINAL1:30;
hence ex b1 being T-Sequence of D st b1 is finite ; ::_thesis: verum
end;
end;
definition
let D be set ;
mode XFinSequence of D is finite T-Sequence of D;
end;
theorem Th12: :: AFINSQ_1:12
for D being set
for f being XFinSequence of D holds f is PartFunc of NAT,D
proof
let D be set ; ::_thesis: for f being XFinSequence of D holds f is PartFunc of NAT,D
let f be XFinSequence of D; ::_thesis: f is PartFunc of NAT,D
( dom f c= NAT & rng f c= D ) by RELAT_1:def_19;
hence f is PartFunc of NAT,D by RELSET_1:4; ::_thesis: verum
end;
registration
cluster Relation-like Function-like empty -> T-Sequence-like for set ;
coherence
for b1 being Function st b1 is empty holds
b1 is T-Sequence-like ;
end;
theorem :: AFINSQ_1:13
for k being Nat
for a being set holds k --> a is XFinSequence ;
theorem Th14: :: AFINSQ_1:14
for k being Nat
for D being non empty set ex p being XFinSequence of D st len p = k
proof
let k be Nat; ::_thesis: for D being non empty set ex p being XFinSequence of D st len p = k
let D be non empty set ; ::_thesis: ex p being XFinSequence of D st len p = k
set y = the Element of D;
set p = k --> the Element of D;
reconsider p = k --> the Element of D as XFinSequence ;
reconsider p = p as XFinSequence of D ;
take p ; ::_thesis: len p = k
thus len p = k by FUNCOP_1:13; ::_thesis: verum
end;
theorem :: AFINSQ_1:15
for p being XFinSequence holds
( len p = 0 iff p = {} ) ;
theorem Th16: :: AFINSQ_1:16
for D being set holds {} is XFinSequence of D
proof
let D be set ; ::_thesis: {} is XFinSequence of D
rng {} c= D by XBOOLE_1:2;
hence {} is XFinSequence of D by RELAT_1:def_19; ::_thesis: verum
end;
registration
let D be set ;
cluster Relation-like D -valued T-Sequence-like Function-like empty finite for set ;
existence
ex b1 being XFinSequence of D st b1 is empty
proof
{} is XFinSequence of D by Th16;
hence ex b1 being XFinSequence of D st b1 is empty ; ::_thesis: verum
end;
end;
registration
let D be non empty set ;
cluster Relation-like D -valued T-Sequence-like Function-like non empty finite for set ;
existence
not for b1 being XFinSequence of D holds b1 is empty
proof
set k = 1;
consider p being XFinSequence of D such that
A1: len p = 1 by Th14;
p <> {} by A1;
hence not for b1 being XFinSequence of D holds b1 is empty ; ::_thesis: verum
end;
end;
definition
let x be set ;
func<%x%> -> set equals :: AFINSQ_1:def 1
0 .--> x;
coherence
0 .--> x is set ;
end;
:: deftheorem defines <% AFINSQ_1:def_1_:_
for x being set holds <%x%> = 0 .--> x;
registration
let x be set ;
cluster<%x%> -> non empty ;
coherence
not <%x%> is empty ;
end;
definition
let D be set ;
func <%> D -> XFinSequence of D equals :: AFINSQ_1:def 2
{} ;
coherence
{} is XFinSequence of D by Th16;
end;
:: deftheorem defines <%> AFINSQ_1:def_2_:_
for D being set holds <%> D = {} ;
registration
let D be set ;
cluster <%> D -> empty ;
coherence
<%> D is empty ;
end;
definition
let p, q be XFinSequence;
redefine func p ^ q means :Def3: :: AFINSQ_1:def 3
( dom it = (len p) + (len q) & ( for k being Nat st k in dom p holds
it . k = p . k ) & ( for k being Nat st k in dom q holds
it . ((len p) + k) = q . k ) );
compatibility
for b1 being set holds
( b1 = p ^ q iff ( dom b1 = (len p) + (len q) & ( for k being Nat st k in dom p holds
b1 . k = p . k ) & ( for k being Nat st k in dom q holds
b1 . ((len p) + k) = q . k ) ) )
proof
let pq be T-Sequence; ::_thesis: ( pq = p ^ q iff ( dom pq = (len p) + (len q) & ( for k being Nat st k in dom p holds
pq . k = p . k ) & ( for k being Nat st k in dom q holds
pq . ((len p) + k) = q . k ) ) )
A1: (len p) +^ (len q) = (len p) + (len q) by CARD_2:36;
hereby ::_thesis: ( dom pq = (len p) + (len q) & ( for k being Nat st k in dom p holds
pq . k = p . k ) & ( for k being Nat st k in dom q holds
pq . ((len p) + k) = q . k ) implies pq = p ^ q )
assume A2: pq = p ^ q ; ::_thesis: ( dom pq = (len p) + (len q) & ( for k being Nat st k in dom p holds
pq . k = p . k ) & ( for k being Nat st k in dom q holds
pq . ((len p) + k) = q . k ) )
hence dom pq = (len p) + (len q) by A1, ORDINAL4:def_1; ::_thesis: ( ( for k being Nat st k in dom p holds
pq . k = p . k ) & ( for k being Nat st k in dom q holds
pq . ((len p) + k) = q . k ) )
thus for k being Nat st k in dom p holds
pq . k = p . k by A2, ORDINAL4:def_1; ::_thesis: for k being Nat st k in dom q holds
pq . ((len p) + k) = q . k
let k be Nat; ::_thesis: ( k in dom q implies pq . ((len p) + k) = q . k )
assume k in dom q ; ::_thesis: pq . ((len p) + k) = q . k
then ( pq . ((len p) +^ k) = q . k & k in NAT ) by A2, ORDINAL4:def_1;
hence pq . ((len p) + k) = q . k by CARD_2:36; ::_thesis: verum
end;
assume that
A3: dom pq = (len p) + (len q) and
A4: for k being Nat st k in dom p holds
pq . k = p . k and
A5: for k being Nat st k in dom q holds
pq . ((len p) + k) = q . k ; ::_thesis: pq = p ^ q
A6: now__::_thesis:_for_a_being_Ordinal_st_a_in_dom_q_holds_
pq_._((dom_p)_+^_a)_=_q_._a
let a be Ordinal; ::_thesis: ( a in dom q implies pq . ((dom p) +^ a) = q . a )
assume A7: a in dom q ; ::_thesis: pq . ((dom p) +^ a) = q . a
then reconsider k = a as Element of NAT ;
thus pq . ((dom p) +^ a) = pq . ((len p) + k) by CARD_2:36
.= q . a by A5, A7 ; ::_thesis: verum
end;
for a being Ordinal st a in dom p holds
pq . a = p . a by A4;
hence pq = p ^ q by A1, A3, A6, ORDINAL4:def_1; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines ^ AFINSQ_1:def_3_:_
for p, q being XFinSequence
for b3 being set holds
( b3 = p ^ q iff ( dom b3 = (len p) + (len q) & ( for k being Nat st k in dom p holds
b3 . k = p . k ) & ( for k being Nat st k in dom q holds
b3 . ((len p) + k) = q . k ) ) );
registration
let p, q be XFinSequence;
clusterp ^ q -> finite ;
coherence
p ^ q is finite
proof
dom (p ^ q) = (dom p) +^ (dom q) by ORDINAL4:def_1;
hence p ^ q is finite by FINSET_1:10; ::_thesis: verum
end;
end;
theorem :: AFINSQ_1:17
for p, q being XFinSequence holds len (p ^ q) = (len p) + (len q) by Def3;
theorem Th18: :: AFINSQ_1:18
for k being Nat
for p, q being XFinSequence st len p <= k & k < (len p) + (len q) holds
(p ^ q) . k = q . (k - (len p))
proof
let k be Nat; ::_thesis: for p, q being XFinSequence st len p <= k & k < (len p) + (len q) holds
(p ^ q) . k = q . (k - (len p))
let p, q be XFinSequence; ::_thesis: ( len p <= k & k < (len p) + (len q) implies (p ^ q) . k = q . (k - (len p)) )
assume that
A1: len p <= k and
A2: k < (len p) + (len q) ; ::_thesis: (p ^ q) . k = q . (k - (len p))
consider m being Nat such that
A3: (len p) + m = k by A1, NAT_1:10;
k - (len p) < ((len p) + (len q)) - (len p) by A2, XREAL_1:14;
then m in dom q by A3, NAT_1:44;
hence (p ^ q) . k = q . (k - (len p)) by A3, Def3; ::_thesis: verum
end;
theorem Th19: :: AFINSQ_1:19
for k being Nat
for p, q being XFinSequence st len p <= k & k < len (p ^ q) holds
(p ^ q) . k = q . (k - (len p))
proof
let k be Nat; ::_thesis: for p, q being XFinSequence st len p <= k & k < len (p ^ q) holds
(p ^ q) . k = q . (k - (len p))
let p, q be XFinSequence; ::_thesis: ( len p <= k & k < len (p ^ q) implies (p ^ q) . k = q . (k - (len p)) )
assume that
A1: len p <= k and
A2: k < len (p ^ q) ; ::_thesis: (p ^ q) . k = q . (k - (len p))
k < (len p) + (len q) by A2, Def3;
hence (p ^ q) . k = q . (k - (len p)) by A1, Th18; ::_thesis: verum
end;
theorem Th20: :: AFINSQ_1:20
for k being Nat
for p, q being XFinSequence holds
( not k in dom (p ^ q) or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
proof
let k be Nat; ::_thesis: for p, q being XFinSequence holds
( not k in dom (p ^ q) or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
let p, q be XFinSequence; ::_thesis: ( not k in dom (p ^ q) or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
assume k in dom (p ^ q) ; ::_thesis: ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
then k in (len p) + (len q) by Def3;
then A1: k < (len p) + (len q) by NAT_1:44;
now__::_thesis:_(_not_len_p_<=_k_or_k_in_dom_p_or_ex_n_being_Nat_st_
(_n_in_dom_q_&_k_=_(len_p)_+_n_)_)
assume len p <= k ; ::_thesis: ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
then consider n being Nat such that
A2: k = (len p) + n by NAT_1:10;
(n + (len p)) - (len p) < ((len q) + (len p)) - (len p) by A1, A2, XREAL_1:14;
then n in len q by NAT_1:44;
hence ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by A2; ::_thesis: verum
end;
hence ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by NAT_1:44; ::_thesis: verum
end;
theorem Th21: :: AFINSQ_1:21
for p, q being T-Sequence holds dom p c= dom (p ^ q)
proof
let p, q be T-Sequence; ::_thesis: dom p c= dom (p ^ q)
dom (p ^ q) = (dom p) +^ (dom q) by ORDINAL4:def_1;
hence dom p c= dom (p ^ q) by ORDINAL3:24; ::_thesis: verum
end;
theorem Th22: :: AFINSQ_1:22
for x being set
for q, p being XFinSequence st x in dom q holds
ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )
proof
let x be set ; ::_thesis: for q, p being XFinSequence st x in dom q holds
ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )
let q, p be XFinSequence; ::_thesis: ( x in dom q implies ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) ) )
assume A1: x in dom q ; ::_thesis: ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )
then reconsider k = x as Element of NAT ;
take k ; ::_thesis: ( k = x & (len p) + k in dom (p ^ q) )
k < len q by A1, NAT_1:44;
then (len p) + k < (len p) + (len q) by XREAL_1:8;
then (len p) + k in (len p) + (len q) by NAT_1:44;
hence ( k = x & (len p) + k in dom (p ^ q) ) by Def3; ::_thesis: verum
end;
theorem Th23: :: AFINSQ_1:23
for k being Nat
for q, p being XFinSequence st k in dom q holds
(len p) + k in dom (p ^ q)
proof
let k be Nat; ::_thesis: for q, p being XFinSequence st k in dom q holds
(len p) + k in dom (p ^ q)
let q, p be XFinSequence; ::_thesis: ( k in dom q implies (len p) + k in dom (p ^ q) )
assume k in dom q ; ::_thesis: (len p) + k in dom (p ^ q)
then ex n being Nat st
( n = k & (len p) + n in dom (p ^ q) ) by Th22;
hence (len p) + k in dom (p ^ q) ; ::_thesis: verum
end;
theorem Th24: :: AFINSQ_1:24
for p, q being XFinSequence holds rng p c= rng (p ^ q)
proof
let p, q be XFinSequence; ::_thesis: rng p c= rng (p ^ q)
now__::_thesis:_for_x_being_set_st_x_in_rng_p_holds_
x_in_rng_(p_^_q)
A1: dom p c= dom (p ^ q) by Th21;
let x be set ; ::_thesis: ( x in rng p implies x in rng (p ^ q) )
assume x in rng p ; ::_thesis: x in rng (p ^ q)
then consider y being set such that
A2: y in dom p and
A3: x = p . y by FUNCT_1:def_3;
reconsider k = y as Element of NAT by A2;
(p ^ q) . k = p . k by A2, Def3;
hence x in rng (p ^ q) by A2, A3, A1, FUNCT_1:3; ::_thesis: verum
end;
hence rng p c= rng (p ^ q) by TARSKI:def_3; ::_thesis: verum
end;
theorem Th25: :: AFINSQ_1:25
for q, p being XFinSequence holds rng q c= rng (p ^ q)
proof
let q, p be XFinSequence; ::_thesis: rng q c= rng (p ^ q)
now__::_thesis:_for_x_being_set_st_x_in_rng_q_holds_
x_in_rng_(p_^_q)
let x be set ; ::_thesis: ( x in rng q implies x in rng (p ^ q) )
assume x in rng q ; ::_thesis: x in rng (p ^ q)
then consider y being set such that
A1: y in dom q and
A2: x = q . y by FUNCT_1:def_3;
reconsider k = y as Element of NAT by A1;
( (len p) + k in dom (p ^ q) & (p ^ q) . ((len p) + k) = q . k ) by A1, Def3, Th23;
hence x in rng (p ^ q) by A2, FUNCT_1:3; ::_thesis: verum
end;
hence rng q c= rng (p ^ q) by TARSKI:def_3; ::_thesis: verum
end;
theorem Th26: :: AFINSQ_1:26
for p, q being XFinSequence holds rng (p ^ q) = (rng p) \/ (rng q)
proof
let p, q be XFinSequence; ::_thesis: rng (p ^ q) = (rng p) \/ (rng q)
now__::_thesis:_for_x_being_set_st_x_in_rng_(p_^_q)_holds_
x_in_(rng_p)_\/_(rng_q)
let x be set ; ::_thesis: ( x in rng (p ^ q) implies x in (rng p) \/ (rng q) )
assume x in rng (p ^ q) ; ::_thesis: x in (rng p) \/ (rng q)
then consider y being set such that
A1: y in dom (p ^ q) and
A2: x = (p ^ q) . y by FUNCT_1:def_3;
reconsider k = y as Element of NAT by A1;
y in (len p) + (len q) by A1, Def3;
then A3: k < (len p) + (len q) by NAT_1:44;
A4: now__::_thesis:_(_len_p_<=_k_implies_x_in_rng_q_)
assume A5: len p <= k ; ::_thesis: x in rng q
then consider m being Nat such that
A6: (len p) + m = k by NAT_1:10;
(m + (len p)) - (len p) < ((len p) + (len q)) - (len p) by A3, A6, XREAL_1:14;
then A7: m in len q by NAT_1:44;
q . (k - (len p)) = x by A2, A3, A5, Th18;
hence x in rng q by A6, A7, FUNCT_1:3; ::_thesis: verum
end;
now__::_thesis:_(_not_len_p_<=_k_implies_x_in_rng_p_)
assume not len p <= k ; ::_thesis: x in rng p
then A8: k in dom p by NAT_1:44;
then p . k = x by A2, Def3;
hence x in rng p by A8, FUNCT_1:3; ::_thesis: verum
end;
hence x in (rng p) \/ (rng q) by A4, XBOOLE_0:def_3; ::_thesis: verum
end;
then A9: rng (p ^ q) c= (rng p) \/ (rng q) by TARSKI:def_3;
( rng p c= rng (p ^ q) & rng q c= rng (p ^ q) ) by Th24, Th25;
then (rng p) \/ (rng q) c= rng (p ^ q) by XBOOLE_1:8;
hence rng (p ^ q) = (rng p) \/ (rng q) by A9, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th27: :: AFINSQ_1:27
for p, q, r being XFinSequence holds (p ^ q) ^ r = p ^ (q ^ r)
proof
let p, q, r be XFinSequence; ::_thesis: (p ^ q) ^ r = p ^ (q ^ r)
A1: for k being Nat st k in dom p holds
((p ^ q) ^ r) . k = p . k
proof
let k be Nat; ::_thesis: ( k in dom p implies ((p ^ q) ^ r) . k = p . k )
assume A2: k in dom p ; ::_thesis: ((p ^ q) ^ r) . k = p . k
dom p c= dom (p ^ q) by Th21;
hence ((p ^ q) ^ r) . k = (p ^ q) . k by A2, Def3
.= p . k by A2, Def3 ;
::_thesis: verum
end;
A3: for k being Nat st k in dom (q ^ r) holds
((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k
proof
let k be Nat; ::_thesis: ( k in dom (q ^ r) implies ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k )
assume A4: k in dom (q ^ r) ; ::_thesis: ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k
A5: now__::_thesis:_(_not_k_in_dom_q_implies_((p_^_q)_^_r)_._((len_p)_+_k)_=_(q_^_r)_._k_)
assume not k in dom q ; ::_thesis: ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k
then consider n being Nat such that
A6: n in dom r and
A7: k = (len q) + n by A4, Th20;
thus ((p ^ q) ^ r) . ((len p) + k) = ((p ^ q) ^ r) . (((len p) + (len q)) + n) by A7
.= ((p ^ q) ^ r) . ((len (p ^ q)) + n) by Def3
.= r . n by A6, Def3
.= (q ^ r) . k by A6, A7, Def3 ; ::_thesis: verum
end;
now__::_thesis:_(_k_in_dom_q_implies_((p_^_q)_^_r)_._((len_p)_+_k)_=_(q_^_r)_._k_)
assume A8: k in dom q ; ::_thesis: ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k
then (len p) + k in dom (p ^ q) by Th23;
hence ((p ^ q) ^ r) . ((len p) + k) = (p ^ q) . ((len p) + k) by Def3
.= q . k by A8, Def3
.= (q ^ r) . k by A8, Def3 ;
::_thesis: verum
end;
hence ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k by A5; ::_thesis: verum
end;
dom ((p ^ q) ^ r) = (len (p ^ q)) + (len r) by Def3
.= ((len p) + (len q)) + (len r) by Def3
.= (len p) + ((len q) + (len r))
.= (len p) + (len (q ^ r)) by Def3 ;
hence (p ^ q) ^ r = p ^ (q ^ r) by A1, A3, Def3; ::_thesis: verum
end;
theorem Th28: :: AFINSQ_1:28
for p, r, q being XFinSequence st ( p ^ r = q ^ r or r ^ p = r ^ q ) holds
p = q
proof
let p, r, q be XFinSequence; ::_thesis: ( ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q )
A1: now__::_thesis:_(_p_^_r_=_q_^_r_&_(_p_^_r_=_q_^_r_or_r_^_p_=_r_^_q_)_implies_p_=_q_)
assume A2: p ^ r = q ^ r ; ::_thesis: ( ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q )
then (len p) + (len r) = len (q ^ r) by Def3;
then A3: (len p) + (len r) = (len q) + (len r) by Def3;
for k being Nat st k in dom p holds
p . k = q . k
proof
let k be Nat; ::_thesis: ( k in dom p implies p . k = q . k )
assume A4: k in dom p ; ::_thesis: p . k = q . k
hence p . k = (q ^ r) . k by A2, Def3
.= q . k by A3, A4, Def3 ;
::_thesis: verum
end;
hence ( ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q ) by A3, Th8; ::_thesis: verum
end;
A5: now__::_thesis:_(_r_^_p_=_r_^_q_&_(_p_^_r_=_q_^_r_or_r_^_p_=_r_^_q_)_implies_p_=_q_)
assume A6: r ^ p = r ^ q ; ::_thesis: ( ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q )
then A7: (len r) + (len p) = len (r ^ q) by Def3
.= (len r) + (len q) by Def3 ;
for k being Nat st k in dom p holds
p . k = q . k
proof
let k be Nat; ::_thesis: ( k in dom p implies p . k = q . k )
assume A8: k in dom p ; ::_thesis: p . k = q . k
hence p . k = (r ^ q) . ((len r) + k) by A6, Def3
.= q . k by A7, A8, Def3 ;
::_thesis: verum
end;
hence ( ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q ) by A7, Th8; ::_thesis: verum
end;
assume ( p ^ r = q ^ r or r ^ p = r ^ q ) ; ::_thesis: p = q
hence p = q by A1, A5; ::_thesis: verum
end;
registration
let p be XFinSequence;
reducep ^ {} to p;
reducibility
p ^ {} = p
proof
A1: for k being Nat st k in dom p holds
p . k = (p ^ {}) . k by Def3;
dom (p ^ {}) = (len p) + (len {}) by Def3
.= dom p ;
hence p ^ {} = p by A1, Th8; ::_thesis: verum
end;
reduce{} ^ p to p;
reducibility
{} ^ p = p
proof
A2: for k being Nat st k in dom p holds
p . k = ({} ^ p) . k
proof
let k be Nat; ::_thesis: ( k in dom p implies p . k = ({} ^ p) . k )
assume A3: k in dom p ; ::_thesis: p . k = ({} ^ p) . k
thus ({} ^ p) . k = ({} ^ p) . ((len {}) + k)
.= p . k by A3, Def3 ; ::_thesis: verum
end;
dom ({} ^ p) = (len {}) + (len p) by Def3
.= dom p ;
hence {} ^ p = p by A2, Th8; ::_thesis: verum
end;
end;
theorem :: AFINSQ_1:29
canceled;
theorem Th30: :: AFINSQ_1:30
for p, q being XFinSequence st p ^ q = {} holds
( p = {} & q = {} )
proof
let p, q be XFinSequence; ::_thesis: ( p ^ q = {} implies ( p = {} & q = {} ) )
assume p ^ q = {} ; ::_thesis: ( p = {} & q = {} )
then 0 = len (p ^ q)
.= (len p) + (len q) by Def3 ;
hence ( p = {} & q = {} ) ; ::_thesis: verum
end;
registration
let D be set ;
let p, q be XFinSequence of D;
clusterp ^ q -> D -valued ;
coherence
p ^ q is D -valued
proof
A1: rng q c= D by RELAT_1:def_19;
( rng (p ^ q) = (rng p) \/ (rng q) & rng p c= D ) by Th26, RELAT_1:def_19;
then rng (p ^ q) c= D by A1, XBOOLE_1:8;
hence p ^ q is D -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;
Lm1: for x, y, x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
proof
let x, y be set ; ::_thesis: for x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
let x1, y1 be set ; ::_thesis: ( [x,y] in {[x1,y1]} implies ( x = x1 & y = y1 ) )
assume [x,y] in {[x1,y1]} ; ::_thesis: ( x = x1 & y = y1 )
then [x,y] = [x1,y1] by TARSKI:def_1;
hence ( x = x1 & y = y1 ) by XTUPLE_0:1; ::_thesis: verum
end;
definition
let x be set ;
:: original: <%
redefine func<%x%> -> Function means :Def4: :: AFINSQ_1:def 4
( dom it = 1 & it . 0 = x );
coherence
<%x%> is Function ;
compatibility
for b1 being Function holds
( b1 = <%x%> iff ( dom b1 = 1 & b1 . 0 = x ) )
proof
let f be Function; ::_thesis: ( f = <%x%> iff ( dom f = 1 & f . 0 = x ) )
thus ( f = <%x%> implies ( dom f = 1 & f . 0 = x ) ) by CARD_1:49, FUNCOP_1:13, FUNCOP_1:72; ::_thesis: ( dom f = 1 & f . 0 = x implies f = <%x%> )
assume that
A1: dom f = 1 and
A2: f . 0 = x ; ::_thesis: f = <%x%>
reconsider g = {[0,(f . 0)]} as Function ;
for y, z being set holds
( [y,z] in f iff [y,z] in g )
proof
let y, z be set ; ::_thesis: ( [y,z] in f iff [y,z] in g )
hereby ::_thesis: ( [y,z] in g implies [y,z] in f )
assume A3: [y,z] in f ; ::_thesis: [y,z] in g
then y in {0} by A1, CARD_1:49, XTUPLE_0:def_12;
then A4: y = 0 by TARSKI:def_1;
A5: rng f = {(f . 0)} by A1, CARD_1:49, FUNCT_1:4;
z in rng f by A3, XTUPLE_0:def_13;
then z = f . 0 by A5, TARSKI:def_1;
hence [y,z] in g by A4, TARSKI:def_1; ::_thesis: verum
end;
assume [y,z] in g ; ::_thesis: [y,z] in f
then A6: ( y = 0 & z = f . 0 ) by Lm1;
0 in dom f by A1, CARD_1:49, TARSKI:def_1;
hence [y,z] in f by A6, FUNCT_1:def_2; ::_thesis: verum
end;
then f = {[0,(f . 0)]} by RELAT_1:def_2;
hence f = <%x%> by A2, FUNCT_4:82; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines <% AFINSQ_1:def_4_:_
for x being set
for b2 being Function holds
( b2 = <%x%> iff ( dom b2 = 1 & b2 . 0 = x ) );
registration
let x be set ;
cluster<%x%> -> Relation-like Function-like ;
coherence
( <%x%> is Function-like & <%x%> is Relation-like ) ;
end;
registration
let x be set ;
cluster<%x%> -> T-Sequence-like finite ;
coherence
( <%x%> is finite & <%x%> is T-Sequence-like )
proof
dom <%x%> = 1 by Def4;
hence ( <%x%> is finite & <%x%> is T-Sequence-like ) by ORDINAL1:def_7; ::_thesis: verum
end;
end;
theorem :: AFINSQ_1:31
for p, q being XFinSequence
for D being set st p ^ q is XFinSequence of D holds
( p is XFinSequence of D & q is XFinSequence of D )
proof
let p, q be XFinSequence; ::_thesis: for D being set st p ^ q is XFinSequence of D holds
( p is XFinSequence of D & q is XFinSequence of D )
let D be set ; ::_thesis: ( p ^ q is XFinSequence of D implies ( p is XFinSequence of D & q is XFinSequence of D ) )
assume p ^ q is XFinSequence of D ; ::_thesis: ( p is XFinSequence of D & q is XFinSequence of D )
then rng (p ^ q) c= D by RELAT_1:def_19;
then A1: (rng p) \/ (rng q) c= D by Th26;
rng p c= (rng p) \/ (rng q) by XBOOLE_1:7;
then rng p c= D by A1, XBOOLE_1:1;
hence p is XFinSequence of D by RELAT_1:def_19; ::_thesis: q is XFinSequence of D
rng q c= (rng p) \/ (rng q) by XBOOLE_1:7;
then rng q c= D by A1, XBOOLE_1:1;
hence q is XFinSequence of D by RELAT_1:def_19; ::_thesis: verum
end;
definition
let x, y be set ;
func<%x,y%> -> set equals :: AFINSQ_1:def 5
<%x%> ^ <%y%>;
correctness
coherence
<%x%> ^ <%y%> is set ;
;
let z be set ;
func<%x,y,z%> -> set equals :: AFINSQ_1:def 6
(<%x%> ^ <%y%>) ^ <%z%>;
correctness
coherence
(<%x%> ^ <%y%>) ^ <%z%> is set ;
;
end;
:: deftheorem defines <% AFINSQ_1:def_5_:_
for x, y being set holds <%x,y%> = <%x%> ^ <%y%>;
:: deftheorem defines <% AFINSQ_1:def_6_:_
for x, y, z being set holds <%x,y,z%> = (<%x%> ^ <%y%>) ^ <%z%>;
registration
let x, y be set ;
cluster<%x,y%> -> Relation-like Function-like ;
coherence
( <%x,y%> is Function-like & <%x,y%> is Relation-like ) ;
let z be set ;
cluster<%x,y,z%> -> Relation-like Function-like ;
coherence
( <%x,y,z%> is Function-like & <%x,y,z%> is Relation-like ) ;
end;
registration
let x, y be set ;
cluster<%x,y%> -> T-Sequence-like finite ;
coherence
( <%x,y%> is finite & <%x,y%> is T-Sequence-like ) ;
let z be set ;
cluster<%x,y,z%> -> T-Sequence-like finite ;
coherence
( <%x,y,z%> is finite & <%x,y,z%> is T-Sequence-like ) ;
end;
theorem :: AFINSQ_1:32
for x being set holds <%x%> = {[0,x]} by FUNCT_4:82;
theorem Th33: :: AFINSQ_1:33
for x being set
for p being XFinSequence holds
( p = <%x%> iff ( dom p = 1 & rng p = {x} ) )
proof
let x be set ; ::_thesis: for p being XFinSequence holds
( p = <%x%> iff ( dom p = 1 & rng p = {x} ) )
let p be XFinSequence; ::_thesis: ( p = <%x%> iff ( dom p = 1 & rng p = {x} ) )
thus ( p = <%x%> implies ( dom p = 1 & rng p = {x} ) ) ::_thesis: ( dom p = 1 & rng p = {x} implies p = <%x%> )
proof
assume A1: p = <%x%> ; ::_thesis: ( dom p = 1 & rng p = {x} )
hence dom p = 1 by Def4; ::_thesis: rng p = {x}
dom p = {0} by A1, Def4, CARD_1:49;
then rng p = {(p . 0)} by FUNCT_1:4;
hence rng p = {x} by A1, Def4; ::_thesis: verum
end;
assume that
A2: dom p = 1 and
A3: rng p = {x} ; ::_thesis: p = <%x%>
1 = 0 + 1 ;
then p . 0 in {x} by A2, A3, FUNCT_1:3, NAT_1:45;
then p . 0 = x by TARSKI:def_1;
hence p = <%x%> by A2, Def4; ::_thesis: verum
end;
theorem :: AFINSQ_1:34
for x being set
for p being XFinSequence holds
( p = <%x%> iff ( len p = 1 & p . 0 = x ) ) by Def4;
theorem Th35: :: AFINSQ_1:35
for x being set
for p being XFinSequence holds (<%x%> ^ p) . 0 = x
proof
let x be set ; ::_thesis: for p being XFinSequence holds (<%x%> ^ p) . 0 = x
let p be XFinSequence; ::_thesis: (<%x%> ^ p) . 0 = x
0 in 1 by CARD_1:49, TARSKI:def_1;
then 0 in dom <%x%> by Def4;
then (<%x%> ^ p) . 0 = <%x%> . 0 by Def3;
hence (<%x%> ^ p) . 0 = x by Def4; ::_thesis: verum
end;
theorem Th36: :: AFINSQ_1:36
for x being set
for p being XFinSequence holds (p ^ <%x%>) . (len p) = x
proof
let x be set ; ::_thesis: for p being XFinSequence holds (p ^ <%x%>) . (len p) = x
let p be XFinSequence; ::_thesis: (p ^ <%x%>) . (len p) = x
( dom <%x%> = 1 & 1 = 0 + 1 ) by Def4;
then A1: 0 in dom <%x%> by NAT_1:45;
(len p) + 0 = len p ;
hence (p ^ <%x%>) . (len p) = <%x%> . 0 by A1, Def3
.= x by Def4 ;
::_thesis: verum
end;
theorem :: AFINSQ_1:37
for x, y, z being set holds
( <%x,y,z%> = <%x%> ^ <%y,z%> & <%x,y,z%> = <%x,y%> ^ <%z%> ) by Th27;
theorem Th38: :: AFINSQ_1:38
for x, y being set
for p being XFinSequence holds
( p = <%x,y%> iff ( len p = 2 & p . 0 = x & p . 1 = y ) )
proof
let x, y be set ; ::_thesis: for p being XFinSequence holds
( p = <%x,y%> iff ( len p = 2 & p . 0 = x & p . 1 = y ) )
let p be XFinSequence; ::_thesis: ( p = <%x,y%> iff ( len p = 2 & p . 0 = x & p . 1 = y ) )
thus ( p = <%x,y%> implies ( len p = 2 & p . 0 = x & p . 1 = y ) ) ::_thesis: ( len p = 2 & p . 0 = x & p . 1 = y implies p = <%x,y%> )
proof
assume A1: p = <%x,y%> ; ::_thesis: ( len p = 2 & p . 0 = x & p . 1 = y )
hence len p = (len <%x%>) + (len <%y%>) by Def3
.= 1 + (len <%y%>) by Th33
.= 1 + 1 by Th33
.= 2 ;
::_thesis: ( p . 0 = x & p . 1 = y )
A2: 0 in {0} by TARSKI:def_1;
then A3: 0 in dom <%y%> by Def4, CARD_1:49;
0 in dom <%x%> by A2, Def4, CARD_1:49;
hence p . 0 = <%x%> . 0 by A1, Def3
.= x by Def4 ;
::_thesis: p . 1 = y
thus p . 1 = (<%x%> ^ <%y%>) . ((len <%x%>) + 0) by A1, Th33
.= <%y%> . 0 by A3, Def3
.= y by Def4 ; ::_thesis: verum
end;
assume that
A4: len p = 2 and
A5: p . 0 = x and
A6: p . 1 = y ; ::_thesis: p = <%x,y%>
A7: for k being Nat st k in dom <%y%> holds
p . ((len <%x%>) + k) = <%y%> . k
proof
let k be Nat; ::_thesis: ( k in dom <%y%> implies p . ((len <%x%>) + k) = <%y%> . k )
assume k in dom <%y%> ; ::_thesis: p . ((len <%x%>) + k) = <%y%> . k
then A8: k in {0} by Def4, CARD_1:49;
thus p . ((len <%x%>) + k) = p . (1 + k) by Th33
.= p . (1 + 0) by A8, TARSKI:def_1
.= <%y%> . 0 by A6, Def4
.= <%y%> . k by A8, TARSKI:def_1 ; ::_thesis: verum
end;
A9: for k being Nat st k in dom <%x%> holds
p . k = <%x%> . k
proof
let k be Nat; ::_thesis: ( k in dom <%x%> implies p . k = <%x%> . k )
assume k in dom <%x%> ; ::_thesis: p . k = <%x%> . k
then k in {0} by Def4, CARD_1:49;
then k = 0 by TARSKI:def_1;
hence p . k = <%x%> . k by A5, Def4; ::_thesis: verum
end;
dom p = 1 + 1 by A4
.= (len <%x%>) + 1 by Th33
.= (len <%x%>) + (len <%y%>) by Th33 ;
hence p = <%x,y%> by A9, A7, Def3; ::_thesis: verum
end;
theorem Th39: :: AFINSQ_1:39
for x, y, z being set
for p being XFinSequence holds
( p = <%x,y,z%> iff ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z ) )
proof
let x, y, z be set ; ::_thesis: for p being XFinSequence holds
( p = <%x,y,z%> iff ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z ) )
let p be XFinSequence; ::_thesis: ( p = <%x,y,z%> iff ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z ) )
thus ( p = <%x,y,z%> implies ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z ) ) ::_thesis: ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z implies p = <%x,y,z%> )
proof
A1: 0 in {0} by TARSKI:def_1;
then A2: 0 in dom <%x%> by Def4, CARD_1:49;
A3: 0 in dom <%z%> by A1, Def4, CARD_1:49;
assume A4: p = <%x,y,z%> ; ::_thesis: ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z )
hence len p = (len <%x,y%>) + (len <%z%>) by Def3
.= 2 + (len <%z%>) by Th38
.= 2 + 1 by Th33
.= 3 ;
::_thesis: ( p . 0 = x & p . 1 = y & p . 2 = z )
thus p . 0 = (<%x%> ^ <%y,z%>) . 0 by A4, Th27
.= <%x%> . 0 by A2, Def3
.= x by Def4 ; ::_thesis: ( p . 1 = y & p . 2 = z )
( 1 in 1 + 1 & len <%x,y%> = 2 ) by Th38, NAT_1:45;
hence p . 1 = <%x,y%> . 1 by A4, Def3
.= y by Th38 ;
::_thesis: p . 2 = z
thus p . 2 = (<%x,y%> ^ <%z%>) . ((len <%x,y%>) + 0) by A4, Th38
.= <%z%> . 0 by A3, Def3
.= z by Def4 ; ::_thesis: verum
end;
assume that
A5: len p = 3 and
A6: p . 0 = x and
A7: p . 1 = y and
A8: p . 2 = z ; ::_thesis: p = <%x,y,z%>
A9: for k being Nat st k in dom <%x,y%> holds
p . k = <%x,y%> . k
proof
A10: len <%x,y%> = 2 by Th38;
let k be Nat; ::_thesis: ( k in dom <%x,y%> implies p . k = <%x,y%> . k )
assume A11: k in dom <%x,y%> ; ::_thesis: p . k = <%x,y%> . k
A12: ( k = 1 implies p . k = <%x,y%> . k ) by A7, Th38;
( k = 0 implies p . k = <%x,y%> . k ) by A6, Th38;
hence p . k = <%x,y%> . k by A11, A10, A12, CARD_1:50, TARSKI:def_2; ::_thesis: verum
end;
A13: for k being Nat st k in dom <%z%> holds
p . ((len <%x,y%>) + k) = <%z%> . k
proof
let k be Nat; ::_thesis: ( k in dom <%z%> implies p . ((len <%x,y%>) + k) = <%z%> . k )
assume k in dom <%z%> ; ::_thesis: p . ((len <%x,y%>) + k) = <%z%> . k
then k in {0} by Def4, CARD_1:49;
then A14: k = 0 by TARSKI:def_1;
hence p . ((len <%x,y%>) + k) = p . (2 + 0) by Th38
.= <%z%> . k by A8, A14, Def4 ;
::_thesis: verum
end;
dom p = 2 + 1 by A5
.= (len <%x,y%>) + 1 by Th38
.= (len <%x,y%>) + (len <%z%>) by Th33 ;
hence p = <%x,y,z%> by A9, A13, Def3; ::_thesis: verum
end;
registration
let x be set ;
cluster<%x%> -> 1 -element ;
coherence
<%x%> is 1 -element
proof
thus card <%x%> = 1 by Th33; :: according to CARD_1:def_7 ::_thesis: verum
end;
let y be set ;
cluster<%x,y%> -> 2 -element ;
coherence
<%x,y%> is 2 -element
proof
thus card <%x,y%> = 2 by Th38; :: according to CARD_1:def_7 ::_thesis: verum
end;
let z be set ;
cluster<%x,y,z%> -> 3 -element ;
coherence
<%x,y,z%> is 3 -element
proof
thus card <%x,y,z%> = 3 by Th39; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;
registration
let n be Nat;
cluster Relation-like T-Sequence-like Function-like finite n -element -> n -defined for set ;
coherence
for b1 being XFinSequence st b1 is n -element holds
b1 is n -defined
proof
let s be XFinSequence; ::_thesis: ( s is n -element implies s is n -defined )
assume card s = n ; :: according to CARD_1:def_7 ::_thesis: s is n -defined
hence dom s c= n ; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;
registration
let n be Nat;
let x be set ;
clustern --> x -> T-Sequence-like finite ;
coherence
( n --> x is finite & n --> x is T-Sequence-like ) ;
end;
registration
let n be Nat;
cluster Relation-like T-Sequence-like Function-like finite n -element for set ;
existence
ex b1 being XFinSequence st b1 is n -element
proof
take n --> 0 ; ::_thesis: n --> 0 is n -element
thus card (n --> 0) = n by FUNCOP_1:13; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;
registration
let n be Nat;
cluster Relation-like n -defined T-Sequence-like Function-like finite n -element -> n -defined total n -element for set ;
coherence
for b1 being n -defined n -element XFinSequence holds b1 is total
proof
let s be n -element XFinSequence; ::_thesis: s is total
card s = n by CARD_1:def_7;
hence dom s = n ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
end;
theorem Th40: :: AFINSQ_1:40
for p being XFinSequence st p <> {} holds
ex q being XFinSequence ex x being set st p = q ^ <%x%>
proof
let p be XFinSequence; ::_thesis: ( p <> {} implies ex q being XFinSequence ex x being set st p = q ^ <%x%> )
assume p <> {} ; ::_thesis: ex q being XFinSequence ex x being set st p = q ^ <%x%>
then consider n being Nat such that
A1: len p = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
set q = p | n;
n <= len p by A1, NAT_1:11;
then ( dom (p | n) = (len p) /\ n & n c= len p ) by NAT_1:39, RELAT_1:61;
then A2: dom (p | n) = n by XBOOLE_1:28;
A3: for x being set st x in dom p holds
p . x = ((p | n) ^ <%(p . ((len p) - 1))%>) . x
proof
let x be set ; ::_thesis: ( x in dom p implies p . x = ((p | n) ^ <%(p . ((len p) - 1))%>) . x )
assume A4: x in dom p ; ::_thesis: p . x = ((p | n) ^ <%(p . ((len p) - 1))%>) . x
then reconsider k = x as Element of NAT ;
A5: now__::_thesis:_(_k_in_n_implies_p_._k_=_((p_|_n)_^_<%(p_._((len_p)_-_1))%>)_._k_)
assume A6: k in n ; ::_thesis: p . k = ((p | n) ^ <%(p . ((len p) - 1))%>) . k
hence p . k = (p | n) . k by A2, FUNCT_1:47
.= ((p | n) ^ <%(p . ((len p) - 1))%>) . k by A2, A6, Def3 ;
::_thesis: verum
end;
A7: now__::_thesis:_(_k_in_{n}_implies_((p_|_n)_^_<%(p_._((len_p)_-_1))%>)_._k_=_p_._k_)
0 in 0 + 1 by NAT_1:45;
then A8: 0 in dom <%(p . ((len p) - 1))%> by Def4;
assume A9: k in {n} ; ::_thesis: ((p | n) ^ <%(p . ((len p) - 1))%>) . k = p . k
hence ((p | n) ^ <%(p . ((len p) - 1))%>) . k = ((p | n) ^ <%(p . ((len p) - 1))%>) . ((len (p | n)) + 0) by A2, TARSKI:def_1
.= <%(p . ((len p) - 1))%> . 0 by A8, Def3
.= p . n by A1, Def4
.= p . k by A9, TARSKI:def_1 ;
::_thesis: verum
end;
k in n \/ {n} by A1, A4, Th2;
hence p . x = ((p | n) ^ <%(p . ((len p) - 1))%>) . x by A5, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
take p | n ; ::_thesis: ex x being set st p = (p | n) ^ <%x%>
take p . ((len p) - 1) ; ::_thesis: p = (p | n) ^ <%(p . ((len p) - 1))%>
dom ((p | n) ^ <%(p . ((len p) - 1))%>) = (len (p | n)) + (len <%(p . ((len p) - 1))%>) by Def3
.= dom p by A1, A2, Th33 ;
hence (p | n) ^ <%(p . ((len p) - 1))%> = p by A3, FUNCT_1:2; ::_thesis: verum
end;
registration
let D be non empty set ;
let d1 be Element of D;
cluster<%d1%> -> D -valued ;
coherence
<%d1%> is D -valued ;
let d2 be Element of D;
cluster<%d1,d2%> -> D -valued ;
coherence
<%d1,d2%> is D -valued ;
let d3 be Element of D;
cluster<%d1,d2,d3%> -> D -valued ;
coherence
<%d1,d2,d3%> is D -valued ;
end;
scheme :: AFINSQ_1:sch 3
IndXSeq{ P1[ XFinSequence] } :
for p being XFinSequence holds P1[p]
provided
A1: P1[ {} ] and
A2: for p being XFinSequence
for x being set st P1[p] holds
P1[p ^ <%x%>]
proof
defpred S1[ Real] means for p being XFinSequence st len p = $1 holds
P1[p];
let p be XFinSequence; ::_thesis: P1[p]
consider X being Subset of REAL such that
A3: for x being Real holds
( x in X iff S1[x] ) from SUBSET_1:sch_3();
for k being Nat holds k in X
proof
defpred S2[ Nat] means $1 in X;
for p being XFinSequence st len p = 0 holds
P1[p]
proof
let p be XFinSequence; ::_thesis: ( len p = 0 implies P1[p] )
assume len p = 0 ; ::_thesis: P1[p]
then p = {} ;
hence P1[p] by A1; ::_thesis: verum
end;
then A4: S2[ 0 ] by A3;
A5: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A6: S2[n] ; ::_thesis: S2[n + 1]
S1[n + 1]
proof
let p be XFinSequence; ::_thesis: ( len p = n + 1 implies P1[p] )
assume A7: len p = n + 1 ; ::_thesis: P1[p]
then p <> {} ;
then consider w being XFinSequence, x being set such that
A8: p = w ^ <%x%> by Th40;
len p = (len w) + (len <%x%>) by A8, Def3
.= (len w) + 1 by Def4 ;
then P1[w] by A3, A6, A7;
hence P1[p] by A8, A2; ::_thesis: verum
end;
hence S2[n + 1] by A3; ::_thesis: verum
end;
thus for k being Nat holds S2[k] from NAT_1:sch_2(A4, A5); ::_thesis: verum
end;
then len p in X ;
hence P1[p] by A3; ::_thesis: verum
end;
theorem :: AFINSQ_1:41
for p, q, r, s being XFinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being XFinSequence st p ^ t = r
proof
defpred S1[ XFinSequence] means for p, q, s being XFinSequence st p ^ q = $1 ^ s & len p <= len $1 holds
ex t being XFinSequence st p ^ t = $1;
A1: for r being XFinSequence
for x being set st S1[r] holds
S1[r ^ <%x%>]
proof
let r be XFinSequence; ::_thesis: for x being set st S1[r] holds
S1[r ^ <%x%>]
let x be set ; ::_thesis: ( S1[r] implies S1[r ^ <%x%>] )
assume A2: for p, q, s being XFinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being XFinSequence st p ^ t = r ; ::_thesis: S1[r ^ <%x%>]
let p, q, s be XFinSequence; ::_thesis: ( p ^ q = (r ^ <%x%>) ^ s & len p <= len (r ^ <%x%>) implies ex t being XFinSequence st p ^ t = r ^ <%x%> )
assume that
A3: p ^ q = (r ^ <%x%>) ^ s and
A4: len p <= len (r ^ <%x%>) ; ::_thesis: ex t being XFinSequence st p ^ t = r ^ <%x%>
A5: now__::_thesis:_(_len_p_<>_len_(r_^_<%x%>)_implies_ex_t_being_XFinSequence_st_p_^_t_=_r_^_<%x%>_)
assume len p <> len (r ^ <%x%>) ; ::_thesis: ex t being XFinSequence st p ^ t = r ^ <%x%>
then len p <> (len r) + (len <%x%>) by Def3;
then A6: len p <> (len r) + 1 by Th33;
len p <= (len r) + (len <%x%>) by A4, Def3;
then A7: len p <= (len r) + 1 by Th33;
p ^ q = r ^ (<%x%> ^ s) by A3, Th27;
then consider t being XFinSequence such that
A8: p ^ t = r by A2, A6, A7, NAT_1:8;
p ^ (t ^ <%x%>) = r ^ <%x%> by A8, Th27;
hence ex t being XFinSequence st p ^ t = r ^ <%x%> ; ::_thesis: verum
end;
now__::_thesis:_(_len_p_=_len_(r_^_<%x%>)_implies_ex_t_being_XFinSequence_st_p_^_t_=_r_^_<%x%>_)
assume A9: len p = len (r ^ <%x%>) ; ::_thesis: ex t being XFinSequence st p ^ t = r ^ <%x%>
A10: for k being Nat st k in dom p holds
p . k = (r ^ <%x%>) . k
proof
let k be Nat; ::_thesis: ( k in dom p implies p . k = (r ^ <%x%>) . k )
assume A11: k in dom p ; ::_thesis: p . k = (r ^ <%x%>) . k
hence p . k = ((r ^ <%x%>) ^ s) . k by A3, Def3
.= (r ^ <%x%>) . k by A9, A11, Def3 ;
::_thesis: verum
end;
p ^ {} = r ^ <%x%> by A9, A10, Th8;
hence ex t being XFinSequence st p ^ t = r ^ <%x%> ; ::_thesis: verum
end;
hence ex t being XFinSequence st p ^ t = r ^ <%x%> by A5; ::_thesis: verum
end;
A12: S1[ {} ]
proof
let p, q, s be XFinSequence; ::_thesis: ( p ^ q = {} ^ s & len p <= len {} implies ex t being XFinSequence st p ^ t = {} )
assume that
p ^ q = {} ^ s and
A13: len p <= len {} ; ::_thesis: ex t being XFinSequence st p ^ t = {}
take {} ; ::_thesis: p ^ {} = {}
thus p ^ {} = {} by A13; ::_thesis: verum
end;
for r being XFinSequence holds S1[r] from AFINSQ_1:sch_3(A12, A1);
hence for p, q, r, s being XFinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being XFinSequence st p ^ t = r ; ::_thesis: verum
end;
definition
let D be set ;
funcD ^omega -> set means :Def7: :: AFINSQ_1:def 7
for x being set holds
( x in it iff x is XFinSequence of D );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is XFinSequence of D )
proof
defpred S1[ set ] means $1 is XFinSequence of D;
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool [:NAT,D:] & S1[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X iff x is XFinSequence of D )
let x be set ; ::_thesis: ( x in X iff x is XFinSequence of D )
thus ( x in X implies x is XFinSequence of D ) by A1; ::_thesis: ( x is XFinSequence of D implies x in X )
assume x is XFinSequence of D ; ::_thesis: x in X
then reconsider p = x as XFinSequence of D ;
reconsider p = p as PartFunc of NAT,D by Th12;
p c= [:NAT,D:] ;
hence x in X by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is XFinSequence of D ) ) & ( for x being set holds
( x in b2 iff x is XFinSequence of D ) ) holds
b1 = b2
proof
defpred S1[ set ] means $1 is XFinSequence of D;
thus for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;
:: deftheorem Def7 defines ^omega AFINSQ_1:def_7_:_
for D, b2 being set holds
( b2 = D ^omega iff for x being set holds
( x in b2 iff x is XFinSequence of D ) );
registration
let D be set ;
clusterD ^omega -> non empty ;
coherence
not D ^omega is empty
proof
set f = the XFinSequence of D;
the XFinSequence of D in D ^omega by Def7;
hence not D ^omega is empty ; ::_thesis: verum
end;
end;
theorem :: AFINSQ_1:42
for x, D being set holds
( x in D ^omega iff x is XFinSequence of D ) by Def7;
theorem :: AFINSQ_1:43
for D being set holds {} in D ^omega
proof
let D be set ; ::_thesis: {} in D ^omega
{} = <%> D ;
hence {} in D ^omega by Def7; ::_thesis: verum
end;
scheme :: AFINSQ_1:sch 4
SepXSeq{ F1() -> non empty set , P1[ XFinSequence] } :
ex X being set st
for x being set holds
( x in X iff ex p being XFinSequence st
( p in F1() ^omega & P1[p] & x = p ) )
proof
defpred S1[ set ] means ex p being XFinSequence st
( P1[p] & $1 = p );
consider Y being set such that
A1: for x being set holds
( x in Y iff ( x in F1() ^omega & S1[x] ) ) from XBOOLE_0:sch_1();
take Y ; ::_thesis: for x being set holds
( x in Y iff ex p being XFinSequence st
( p in F1() ^omega & P1[p] & x = p ) )
for x being set st x in Y holds
ex p being XFinSequence st
( p in F1() ^omega & P1[p] & x = p )
proof
let x be set ; ::_thesis: ( x in Y implies ex p being XFinSequence st
( p in F1() ^omega & P1[p] & x = p ) )
assume x in Y ; ::_thesis: ex p being XFinSequence st
( p in F1() ^omega & P1[p] & x = p )
then ( x in F1() ^omega & ex p being XFinSequence st
( P1[p] & x = p ) ) by A1;
hence ex p being XFinSequence st
( p in F1() ^omega & P1[p] & x = p ) ; ::_thesis: verum
end;
hence for x being set holds
( x in Y iff ex p being XFinSequence st
( p in F1() ^omega & P1[p] & x = p ) ) by A1; ::_thesis: verum
end;
notation
let p be XFinSequence;
let i, x be set ;
synonym Replace (p,i,x) for p +* (i,x);
end;
registration
let p be XFinSequence;
let i, x be set ;
cluster Replace (p,i,x) -> T-Sequence-like finite ;
coherence
( p +* (i,x) is finite & p +* (i,x) is T-Sequence-like )
proof
dom (p +* (i,x)) = dom p by FUNCT_7:30;
hence ( p +* (i,x) is finite & p +* (i,x) is T-Sequence-like ) by FINSET_1:10, ORDINAL1:def_7; ::_thesis: verum
end;
end;
theorem :: AFINSQ_1:44
for p being XFinSequence
for i being Element of NAT
for x being set holds
( len (Replace (p,i,x)) = len p & ( i < len p implies (Replace (p,i,x)) . i = x ) & ( for j being Element of NAT st j <> i holds
(Replace (p,i,x)) . j = p . j ) )
proof
let p be XFinSequence; ::_thesis: for i being Element of NAT
for x being set holds
( len (Replace (p,i,x)) = len p & ( i < len p implies (Replace (p,i,x)) . i = x ) & ( for j being Element of NAT st j <> i holds
(Replace (p,i,x)) . j = p . j ) )
let i be Element of NAT ; ::_thesis: for x being set holds
( len (Replace (p,i,x)) = len p & ( i < len p implies (Replace (p,i,x)) . i = x ) & ( for j being Element of NAT st j <> i holds
(Replace (p,i,x)) . j = p . j ) )
let x be set ; ::_thesis: ( len (Replace (p,i,x)) = len p & ( i < len p implies (Replace (p,i,x)) . i = x ) & ( for j being Element of NAT st j <> i holds
(Replace (p,i,x)) . j = p . j ) )
set f = Replace (p,i,x);
thus len (Replace (p,i,x)) = len p by FUNCT_7:30; ::_thesis: ( ( i < len p implies (Replace (p,i,x)) . i = x ) & ( for j being Element of NAT st j <> i holds
(Replace (p,i,x)) . j = p . j ) )
( i < len p implies not dom p c= i ) by NAT_1:39;
hence ( i < len p implies (Replace (p,i,x)) . i = x ) by FUNCT_7:31, ORDINAL1:16; ::_thesis: for j being Element of NAT st j <> i holds
(Replace (p,i,x)) . j = p . j
thus for j being Element of NAT st j <> i holds
(Replace (p,i,x)) . j = p . j by FUNCT_7:32; ::_thesis: verum
end;
registration
let D be non empty set ;
let p be XFinSequence of D;
let i be Element of NAT ;
let a be Element of D;
cluster Replace (p,i,a) -> D -valued ;
coherence
Replace (p,i,a) is D -valued
proof
percases ( i in dom p or not i in dom p ) ;
suppose i in dom p ; ::_thesis: Replace (p,i,a) is D -valued
then Replace (p,i,a) = p +* (i .--> a) by FUNCT_7:def_3;
then A1: rng (Replace (p,i,a)) c= (rng p) \/ (rng (i .--> a)) by FUNCT_4:17;
rng (i .--> a) = {a} by FUNCOP_1:8;
then A2: rng (i .--> a) c= D by ZFMISC_1:31;
rng p c= D by RELAT_1:def_19;
then (rng p) \/ (rng (i .--> a)) c= D by A2, XBOOLE_1:8;
hence rng (Replace (p,i,a)) c= D by A1, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;
suppose not i in dom p ; ::_thesis: Replace (p,i,a) is D -valued
then Replace (p,i,a) = p by FUNCT_7:def_3;
hence rng (Replace (p,i,a)) c= D by RELAT_1:def_19; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;
end;
end;
registration
cluster Relation-like REAL -valued T-Sequence-like Function-like finite -> real-valued for set ;
coherence
for b1 being XFinSequence of REAL holds b1 is real-valued
proof
let F be XFinSequence of REAL ; ::_thesis: F is real-valued
rng F c= REAL by RELAT_1:def_19;
hence F is real-valued by VALUED_0:def_3; ::_thesis: verum
end;
end;
registration
cluster Relation-like NAT -valued T-Sequence-like Function-like finite -> natural-valued for set ;
coherence
for b1 being XFinSequence of NAT holds b1 is natural-valued
proof
let F be XFinSequence of NAT ; ::_thesis: F is natural-valued
rng F c= NAT by RELAT_1:def_19;
hence F is natural-valued by VALUED_0:def_6; ::_thesis: verum
end;
end;
theorem Th45: :: AFINSQ_1:45
for p being XFinSequence
for x1, x2, x3, x4 being set st p = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%> holds
( len p = 4 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 )
proof
let p be XFinSequence; ::_thesis: for x1, x2, x3, x4 being set st p = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%> holds
( len p = 4 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 )
let x1, x2, x3, x4 be set ; ::_thesis: ( p = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%> implies ( len p = 4 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 ) )
assume A1: p = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%> ; ::_thesis: ( len p = 4 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 )
set p13 = (<%x1%> ^ <%x2%>) ^ <%x3%>;
A2: (<%x1%> ^ <%x2%>) ^ <%x3%> = <%x1,x2,x3%> ;
then A3: len ((<%x1%> ^ <%x2%>) ^ <%x3%>) = 3 by Th39;
A4: ( ((<%x1%> ^ <%x2%>) ^ <%x3%>) . 0 = x1 & ((<%x1%> ^ <%x2%>) ^ <%x3%>) . 1 = x2 ) by A2, Th39;
A5: ((<%x1%> ^ <%x2%>) ^ <%x3%>) . 2 = x3 by A2, Th39;
thus len p = (len ((<%x1%> ^ <%x2%>) ^ <%x3%>)) + (len <%x4%>) by A1, Def3
.= 3 + 1 by A3, Th33
.= 4 ; ::_thesis: ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 )
( 0 in 3 & 1 in 3 & 2 in 3 ) by CARD_1:51, ENUMSET1:def_1;
hence ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 ) by A1, A4, A5, Def3, A3; ::_thesis: p . 3 = x4
thus p . 3 = p . (len ((<%x1%> ^ <%x2%>) ^ <%x3%>)) by A2, Th39
.= x4 by A1, Th36 ; ::_thesis: verum
end;
theorem Th46: :: AFINSQ_1:46
for p being XFinSequence
for x1, x2, x3, x4, x5 being set st p = (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%> holds
( len p = 5 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 )
proof
let p be XFinSequence; ::_thesis: for x1, x2, x3, x4, x5 being set st p = (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%> holds
( len p = 5 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 )
let x1, x2, x3, x4, x5 be set ; ::_thesis: ( p = (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%> implies ( len p = 5 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 ) )
assume A1: p = (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%> ; ::_thesis: ( len p = 5 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 )
set p14 = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>;
A2: len (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) = 4 by Th45;
A3: ( (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) . 0 = x1 & (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) . 1 = x2 ) by Th45;
A4: ( (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) . 2 = x3 & (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) . 3 = x4 ) by Th45;
thus len p = (len (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>)) + (len <%x5%>) by A1, Def3
.= 4 + 1 by A2, Th33
.= 5 ; ::_thesis: ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 )
( 0 in 4 & 1 in 4 & 2 in 4 & 3 in 4 ) by CARD_1:52, ENUMSET1:def_2;
hence ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 ) by A1, A3, A4, Def3, A2; ::_thesis: p . 4 = x5
thus p . 4 = p . (len (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>)) by Th45
.= x5 by A1, Th36 ; ::_thesis: verum
end;
theorem Th47: :: AFINSQ_1:47
for p being XFinSequence
for x1, x2, x3, x4, x5, x6 being set st p = ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%> holds
( len p = 6 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 )
proof
let p be XFinSequence; ::_thesis: for x1, x2, x3, x4, x5, x6 being set st p = ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%> holds
( len p = 6 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 )
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: ( p = ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%> implies ( len p = 6 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 ) )
assume A1: p = ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%> ; ::_thesis: ( len p = 6 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 )
set p15 = (((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>;
A2: len ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) = 5 by Th46;
A3: ( ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) . 0 = x1 & ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) . 1 = x2 ) by Th46;
A4: ( ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) . 2 = x3 & ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) . 3 = x4 ) by Th46;
A5: ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) . 4 = x5 by Th46;
thus len p = (len ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>)) + (len <%x6%>) by A1, Def3
.= 5 + 1 by A2, Th33
.= 6 ; ::_thesis: ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 )
( 0 in 5 & 1 in 5 & 2 in 5 & 3 in 5 & 4 in 5 ) by CARD_1:53, ENUMSET1:def_3;
hence ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 ) by A1, A3, A4, A5, Def3, A2; ::_thesis: p . 5 = x6
thus p . 5 = p . (len ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>)) by Th46
.= x6 by A1, Th36 ; ::_thesis: verum
end;
theorem Th48: :: AFINSQ_1:48
for p being XFinSequence
for x1, x2, x3, x4, x5, x6, x7 being set st p = (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%> holds
( len p = 7 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 )
proof
let p be XFinSequence; ::_thesis: for x1, x2, x3, x4, x5, x6, x7 being set st p = (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%> holds
( len p = 7 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 )
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: ( p = (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%> implies ( len p = 7 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 ) )
assume A1: p = (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%> ; ::_thesis: ( len p = 7 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 )
set p16 = ((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>;
A2: len (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) = 6 by Th47;
A3: ( (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) . 0 = x1 & (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) . 1 = x2 ) by Th47;
A4: ( (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) . 2 = x3 & (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) . 3 = x4 ) by Th47;
A5: ( (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) . 4 = x5 & (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) . 5 = x6 ) by Th47;
thus len p = (len (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>)) + (len <%x7%>) by A1, Def3
.= 6 + 1 by A2, Th33
.= 7 ; ::_thesis: ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 )
( 0 in 6 & 1 in 6 & 2 in 6 & 3 in 6 & 4 in 6 & 5 in 6 ) by CARD_1:54, ENUMSET1:def_4;
hence ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 ) by A1, A3, A4, A5, Def3, A2; ::_thesis: p . 6 = x7
thus p . 6 = p . (len (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>)) by Th47
.= x7 by A1, Th36 ; ::_thesis: verum
end;
theorem Th49: :: AFINSQ_1:49
for p being XFinSequence
for x1, x2, x3, x4, x5, x6, x7, x8 being set st p = ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%> holds
( len p = 8 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 & p . 7 = x8 )
proof
let p be XFinSequence; ::_thesis: for x1, x2, x3, x4, x5, x6, x7, x8 being set st p = ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%> holds
( len p = 8 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 & p . 7 = x8 )
let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: ( p = ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%> implies ( len p = 8 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 & p . 7 = x8 ) )
assume A1: p = ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%> ; ::_thesis: ( len p = 8 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 & p . 7 = x8 )
set p17 = (((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>;
A2: len ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) = 7 by Th48;
A3: ( ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) . 0 = x1 & ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) . 1 = x2 ) by Th48;
A4: ( ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) . 2 = x3 & ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) . 3 = x4 ) by Th48;
A5: ( ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) . 4 = x5 & ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) . 5 = x6 ) by Th48;
A6: ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) . 6 = x7 by Th48;
thus len p = (len ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>)) + (len <%x8%>) by A1, Def3
.= 7 + 1 by A2, Th33
.= 8 ; ::_thesis: ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 & p . 7 = x8 )
( 0 in 7 & 1 in 7 & 2 in 7 & 3 in 7 & 4 in 7 & 5 in 7 & 6 in 7 ) by CARD_1:55, ENUMSET1:def_5;
hence ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 ) by A1, A3, A4, A5, A6, Def3, A2; ::_thesis: p . 7 = x8
thus p . 7 = p . (len ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>)) by Th48
.= x8 by A1, Th36 ; ::_thesis: verum
end;
theorem :: AFINSQ_1:50
for p being XFinSequence
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st p = (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) ^ <%x9%> holds
( len p = 9 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 & p . 7 = x8 & p . 8 = x9 )
proof
let p be XFinSequence; ::_thesis: for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st p = (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) ^ <%x9%> holds
( len p = 9 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 & p . 7 = x8 & p . 8 = x9 )
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: ( p = (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) ^ <%x9%> implies ( len p = 9 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 & p . 7 = x8 & p . 8 = x9 ) )
assume A1: p = (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) ^ <%x9%> ; ::_thesis: ( len p = 9 & p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 & p . 7 = x8 & p . 8 = x9 )
set p17 = ((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>;
A2: len (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) = 8 by Th49;
A3: ( (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 0 = x1 & (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 1 = x2 ) by Th49;
A4: ( (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 2 = x3 & (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 3 = x4 ) by Th49;
A5: ( (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 4 = x5 & (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 5 = x6 ) by Th49;
A6: ( (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 6 = x7 & (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>) . 7 = x8 ) by Th49;
thus len p = (len (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>)) + (len <%x9%>) by A1, Def3
.= 8 + 1 by A2, Th33
.= 9 ; ::_thesis: ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 & p . 7 = x8 & p . 8 = x9 )
( 0 in 8 & 1 in 8 & 2 in 8 & 3 in 8 & 4 in 8 & 5 in 8 & 6 in 8 & 7 in 8 ) by CARD_1:56, ENUMSET1:def_6;
hence ( p . 0 = x1 & p . 1 = x2 & p . 2 = x3 & p . 3 = x4 & p . 4 = x5 & p . 5 = x6 & p . 6 = x7 & p . 7 = x8 ) by A1, A3, A4, A5, A6, Def3, A2; ::_thesis: p . 8 = x9
thus p . 8 = p . (len (((((((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>) ^ <%x5%>) ^ <%x6%>) ^ <%x7%>) ^ <%x8%>)) by Th49
.= x9 by A1, Th36 ; ::_thesis: verum
end;
theorem :: AFINSQ_1:51
for n being Nat
for p, q being XFinSequence st n < len p holds
(p ^ q) . n = p . n
proof
let n be Nat; ::_thesis: for p, q being XFinSequence st n < len p holds
(p ^ q) . n = p . n
let p, q be XFinSequence; ::_thesis: ( n < len p implies (p ^ q) . n = p . n )
assume n < len p ; ::_thesis: (p ^ q) . n = p . n
then n in dom p by NAT_1:44;
hence (p ^ q) . n = p . n by Def3; ::_thesis: verum
end;
theorem :: AFINSQ_1:52
for n being Nat
for p being XFinSequence st len p <= n holds
p | n = p
proof
let n be Nat; ::_thesis: for p being XFinSequence st len p <= n holds
p | n = p
let p be XFinSequence; ::_thesis: ( len p <= n implies p | n = p )
assume len p <= n ; ::_thesis: p | n = p
then (len p) /\ n = len p by NAT_1:46;
hence p | n = p by RELAT_1:68, XBOOLE_1:18; ::_thesis: verum
end;
theorem Th53: :: AFINSQ_1:53
for n, k being Nat
for p being XFinSequence st n <= len p & k in n holds
( (p | n) . k = p . k & k in dom p )
proof
let n, k be Nat; ::_thesis: for p being XFinSequence st n <= len p & k in n holds
( (p | n) . k = p . k & k in dom p )
let p be XFinSequence; ::_thesis: ( n <= len p & k in n implies ( (p | n) . k = p . k & k in dom p ) )
assume that
A1: n <= len p and
A2: k in n ; ::_thesis: ( (p | n) . k = p . k & k in dom p )
A3: n c= dom p by A1, NAT_1:39;
then n = (dom p) /\ n by XBOOLE_1:28
.= dom (p | n) by RELAT_1:61 ;
hence ( (p | n) . k = p . k & k in dom p ) by A2, A3, FUNCT_1:47; ::_thesis: verum
end;
theorem Th54: :: AFINSQ_1:54
for n being Nat
for p being XFinSequence st n <= len p holds
len (p | n) = n
proof
let n be Nat; ::_thesis: for p being XFinSequence st n <= len p holds
len (p | n) = n
let p be XFinSequence; ::_thesis: ( n <= len p implies len (p | n) = n )
assume n <= len p ; ::_thesis: len (p | n) = n
then n c= len p by NAT_1:39;
hence len (p | n) = n by RELAT_1:62; ::_thesis: verum
end;
theorem :: AFINSQ_1:55
for n being Nat
for p being XFinSequence holds len (p | n) <= n
proof
let n be Nat; ::_thesis: for p being XFinSequence holds len (p | n) <= n
let p be XFinSequence; ::_thesis: len (p | n) <= n
dom (p | n) c= n by RELAT_1:58;
hence len (p | n) <= n by NAT_1:39; ::_thesis: verum
end;
theorem Th56: :: AFINSQ_1:56
for n being Nat
for p being XFinSequence st len p = n + 1 holds
p = (p | n) ^ <%(p . n)%>
proof
let n be Nat; ::_thesis: for p being XFinSequence st len p = n + 1 holds
p = (p | n) ^ <%(p . n)%>
let p be XFinSequence; ::_thesis: ( len p = n + 1 implies p = (p | n) ^ <%(p . n)%> )
set pn = p | n;
set x = p . n;
assume A1: len p = n + 1 ; ::_thesis: p = (p | n) ^ <%(p . n)%>
then A2: n < len p by NAT_1:13;
then A3: len (p | n) = n by Th54;
A4: now__::_thesis:_for_m_being_Nat_st_m_in_dom_p_holds_
p_._m_=_((p_|_n)_^_<%(p_._n)%>)_._m
let m be Nat; ::_thesis: ( m in dom p implies p . m = ((p | n) ^ <%(p . n)%>) . m )
assume m in dom p ; ::_thesis: p . m = ((p | n) ^ <%(p . n)%>) . m
then m < len p by NAT_1:44;
then A5: m <= len (p | n) by A1, A3, NAT_1:13;
now__::_thesis:_(_(_m_=_len_(p_|_n)_&_p_._m_=_((p_|_n)_^_<%(p_._n)%>)_._m_)_or_(_m_<>_len_(p_|_n)_&_((p_|_n)_^_<%(p_._n)%>)_._m_=_p_._m_)_)
percases ( m = len (p | n) or m <> len (p | n) ) ;
case m = len (p | n) ; ::_thesis: p . m = ((p | n) ^ <%(p . n)%>) . m
hence p . m = ((p | n) ^ <%(p . n)%>) . m by A3, Th36; ::_thesis: verum
end;
case m <> len (p | n) ; ::_thesis: ((p | n) ^ <%(p . n)%>) . m = p . m
then m < len (p | n) by A5, XXREAL_0:1;
then A6: m in dom (p | n) by NAT_1:44;
hence ((p | n) ^ <%(p . n)%>) . m = (p | n) . m by Def3
.= p . m by A2, A3, A6, Th53 ;
::_thesis: verum
end;
end;
end;
hence p . m = ((p | n) ^ <%(p . n)%>) . m ; ::_thesis: verum
end;
len ((p | n) ^ <%(p . n)%>) = n + (len <%(p . n)%>) by A3, Def3
.= len p by A1, Def4 ;
hence p = (p | n) ^ <%(p . n)%> by A4, Th8; ::_thesis: verum
end;
theorem Th57: :: AFINSQ_1:57
for p, q being XFinSequence holds (p ^ q) | (dom p) = p
proof
let p, q be XFinSequence; ::_thesis: (p ^ q) | (dom p) = p
set r = (p ^ q) | (dom p);
A1: now__::_thesis:_for_k_being_Nat_st_k_<_len_p_holds_
((p_^_q)_|_(dom_p))_._k_=_p_._k
let k be Nat; ::_thesis: ( k < len p implies ((p ^ q) | (dom p)) . k = p . k )
assume A2: k < len p ; ::_thesis: ((p ^ q) | (dom p)) . k = p . k
A3: k in dom p by A2, NAT_1:44;
then A4: (p ^ q) . k = p . k by Def3;
k + 0 < (len p) + (len q) by A2, XREAL_1:8;
then k in (len p) + (len q) by NAT_1:44;
then k in dom (p ^ q) by Def3;
then k in (dom (p ^ q)) /\ (dom p) by A3, XBOOLE_0:def_4;
hence ((p ^ q) | (dom p)) . k = p . k by A4, FUNCT_1:48; ::_thesis: verum
end;
dom p c= dom (p ^ q) by Th21;
then len ((p ^ q) | (dom p)) = len p by RELAT_1:62;
hence (p ^ q) | (dom p) = p by A1, Th9; ::_thesis: verum
end;
theorem :: AFINSQ_1:58
for n being Nat
for p, q being XFinSequence st n <= dom p holds
(p ^ q) | n = p | n
proof
let n be Nat; ::_thesis: for p, q being XFinSequence st n <= dom p holds
(p ^ q) | n = p | n
let p, q be XFinSequence; ::_thesis: ( n <= dom p implies (p ^ q) | n = p | n )
assume n <= dom p ; ::_thesis: (p ^ q) | n = p | n
then n c= dom p by NAT_1:39;
then ((p ^ q) | (dom p)) | n = (p ^ q) | n by RELAT_1:74;
hence (p ^ q) | n = p | n by Th57; ::_thesis: verum
end;
theorem :: AFINSQ_1:59
for n, k being Nat
for p, q being XFinSequence st n = (dom p) + k holds
(p ^ q) | n = p ^ (q | k)
proof
let n, k be Nat; ::_thesis: for p, q being XFinSequence st n = (dom p) + k holds
(p ^ q) | n = p ^ (q | k)
let p, q be XFinSequence; ::_thesis: ( n = (dom p) + k implies (p ^ q) | n = p ^ (q | k) )
assume A1: n = (dom p) + k ; ::_thesis: (p ^ q) | n = p ^ (q | k)
now__::_thesis:_(p_^_q)_|_n_=_p_^_(q_|_k)
percases ( n >= len (p ^ q) or n < len (p ^ q) ) ;
supposeA2: n >= len (p ^ q) ; ::_thesis: (p ^ q) | n = p ^ (q | k)
then n >= (len p) + (len q) by Def3;
then k >= len q by A1, XREAL_1:8;
then dom q c= k by NAT_1:39;
then A3: q | k = q by RELAT_1:68;
dom (p ^ q) c= n by A2, NAT_1:39;
hence (p ^ q) | n = p ^ (q | k) by A3, RELAT_1:68; ::_thesis: verum
end;
supposeA4: n < len (p ^ q) ; ::_thesis: (p ^ q) | n = p ^ (q | k)
then A5: len ((p ^ q) | n) = n by Th11;
n < (len p) + (len q) by A4, Def3;
then k < len q by A1, XREAL_1:6;
then len (q | k) = k by Th11;
then A6: len (p ^ (q | k)) = (len p) + k by Def3;
now__::_thesis:_for_m_being_Nat_st_m_in_dom_((p_^_q)_|_n)_holds_
((p_^_q)_|_n)_._m_=_(p_^_(q_|_k))_._m
let m be Nat; ::_thesis: ( m in dom ((p ^ q) | n) implies ((p ^ q) | n) . m = (p ^ (q | k)) . m )
assume A7: m in dom ((p ^ q) | n) ; ::_thesis: ((p ^ q) | n) . m = (p ^ (q | k)) . m
A8: m < len ((p ^ q) | n) by A7, NAT_1:44;
then m < len (p ^ q) by A4, A5, XXREAL_0:2;
then A9: m in len (p ^ q) by NAT_1:44;
m in n by A4, Th11, A7;
then A10: m in (dom (p ^ q)) /\ n by A9, XBOOLE_0:def_4;
then A11: ((p ^ q) | n) . m = (p ^ q) . m by FUNCT_1:48;
now__::_thesis:_((p_^_q)_|_n)_._m_=_(p_^_(q_|_k))_._m
percases ( m < dom p or m >= dom p ) ;
suppose m < dom p ; ::_thesis: ((p ^ q) | n) . m = (p ^ (q | k)) . m
then m in dom p by NAT_1:44;
then ( (p ^ (q | k)) . m = p . m & (p ^ q) . m = p . m ) by Def3;
hence ((p ^ q) | n) . m = (p ^ (q | k)) . m by A10, FUNCT_1:48; ::_thesis: verum
end;
supposeA12: m >= dom p ; ::_thesis: ((p ^ q) | n) . m = (p ^ (q | k)) . m
m < len (p ^ q) by A4, A5, A8, XXREAL_0:2;
then A13: q . (m - (len p)) = (p ^ q) . m by A12, Th19;
A14: (m - (len p)) + (len p) < len (p ^ q) by A4, A5, A8, XXREAL_0:2;
A15: m - (len p) is Nat by A12, NAT_1:21;
len (p ^ q) = (len p) + (len q) by Def3;
then m - (len p) < len q by A14, XREAL_1:6;
then A16: m - (len p) in len q by A15, NAT_1:44;
m - (len p) < k by A1, A5, A14, A8, XREAL_1:6;
then m - (len p) in k by A15, NAT_1:44;
then A17: m - (len p) in k /\ (dom q) by A16, XBOOLE_0:def_4;
(p ^ (q | k)) . m = (q | k) . (m - (len p)) by A1, A6, A5, A12, A8, Th19;
hence ((p ^ q) | n) . m = (p ^ (q | k)) . m by A11, A13, A17, FUNCT_1:48; ::_thesis: verum
end;
end;
end;
hence ((p ^ q) | n) . m = (p ^ (q | k)) . m ; ::_thesis: verum
end;
hence (p ^ q) | n = p ^ (q | k) by Th8, A6, A1, A4, Th11; ::_thesis: verum
end;
end;
end;
hence (p ^ q) | n = p ^ (q | k) ; ::_thesis: verum
end;
theorem :: AFINSQ_1:60
for n being Nat
for p being XFinSequence ex q being XFinSequence st p = (p | n) ^ q
proof
let n be Nat; ::_thesis: for p being XFinSequence ex q being XFinSequence st p = (p | n) ^ q
let p be XFinSequence; ::_thesis: ex q being XFinSequence st p = (p | n) ^ q
now__::_thesis:_ex_q_being_XFinSequence_st_p_=_(p_|_n)_^_q
percases ( n > len p or n <= len p ) ;
suppose n > len p ; ::_thesis: ex q being XFinSequence st p = (p | n) ^ q
then len p c= n by NAT_1:39;
then A1: p | n = p by RELAT_1:68;
p ^ {} = p ;
hence ex q being XFinSequence st p = (p | n) ^ q by A1; ::_thesis: verum
end;
suppose n <= len p ; ::_thesis: ex q being XFinSequence st p = (p | n) ^ q
then reconsider n1 = (len p) - n as Element of NAT by NAT_1:21;
defpred S1[ Nat] means for k being Nat st k = (len p) - $1 holds
ex q being XFinSequence st p = (p | k) ^ q;
A2: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A3: S1[m] ; ::_thesis: S1[m + 1]
let k be Nat; ::_thesis: ( k = (len p) - (m + 1) implies ex q being XFinSequence st p = (p | k) ^ q )
assume A4: k = (len p) - (m + 1) ; ::_thesis: ex q being XFinSequence st p = (p | k) ^ q
consider q being XFinSequence such that
A5: p = (p | (k + 1)) ^ q by A3, A4;
k <= k + 1 by NAT_1:11;
then k c= k + 1 by NAT_1:39;
then A6: (p | (k + 1)) | k = p | k by RELAT_1:74;
(len p) - m <= (len p) - 0 by XREAL_1:10;
then len (p | (k + 1)) = k + 1 by Th54, A4;
then p | (k + 1) = ((p | (k + 1)) | k) ^ <%((p | (k + 1)) . k)%> by Th56;
then p = (p | k) ^ (<%((p | (k + 1)) . k)%> ^ q) by A5, A6, Th27;
hence ex q being XFinSequence st p = (p | k) ^ q ; ::_thesis: verum
end;
( p | ((len p) - 0) = p & p ^ {} = p ) by RELAT_1:68;
then A7: S1[ 0 ] ;
A8: for m being Nat holds S1[m] from NAT_1:sch_2(A7, A2);
n = (len p) - n1 ;
hence ex q being XFinSequence st p = (p | n) ^ q by A8; ::_thesis: verum
end;
end;
end;
hence ex q being XFinSequence st p = (p | n) ^ q ; ::_thesis: verum
end;
theorem :: AFINSQ_1:61
for n, k being Nat
for p being XFinSequence st len p = n + k holds
ex q1, q2 being XFinSequence st
( len q1 = n & len q2 = k & p = q1 ^ q2 )
proof
let n, k be Nat; ::_thesis: for p being XFinSequence st len p = n + k holds
ex q1, q2 being XFinSequence st
( len q1 = n & len q2 = k & p = q1 ^ q2 )
let p be XFinSequence; ::_thesis: ( len p = n + k implies ex q1, q2 being XFinSequence st
( len q1 = n & len q2 = k & p = q1 ^ q2 ) )
defpred S1[ Nat] means for p being XFinSequence
for i, j being Nat st len p = $1 & len p = i + j holds
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 );
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
thus S1[n + 1] ::_thesis: verum
proof
let p be XFinSequence; ::_thesis: for i, j being Nat st len p = n + 1 & len p = i + j holds
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
let i, j be Nat; ::_thesis: ( len p = n + 1 & len p = i + j implies ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 ) )
assume that
A3: len p = n + 1 and
A4: len p = i + j ; ::_thesis: ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
percases ( j = 0 or j > 0 ) ;
supposeA5: j = 0 ; ::_thesis: ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
take q1 = p; ::_thesis: ex q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
take q2 = {} ; ::_thesis: ( len q1 = i & len q2 = j & p = q1 ^ q2 )
p ^ {} = p ;
hence ( len q1 = i & len q2 = j & p = q1 ^ q2 ) by A4, A5; ::_thesis: verum
end;
suppose j > 0 ; ::_thesis: ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
then consider k being Nat such that
A6: j = k + 1 by NAT_1:6;
p <> {} by A3;
then consider q being XFinSequence, x being set such that
A7: p = q ^ <%x%> by Th40;
A8: n + 1 = (len q) + (len <%x%>) by A3, A7, Def3
.= (len q) + 1 by Th33 ;
n = i + k by A3, A4, A6;
then consider q1, q2 being XFinSequence such that
A9: len q1 = i and
A10: len q2 = k and
A11: q = q1 ^ q2 by A2, A8;
A12: len (q2 ^ <%x%>) = (len q2) + (len <%x%>) by Def3
.= j by A6, A10, Th33 ;
p = q1 ^ (q2 ^ <%x%>) by A7, A11, Th27;
hence ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 ) by A9, A12; ::_thesis: verum
end;
end;
end;
end;
A13: S1[ 0 ]
proof
let p be XFinSequence; ::_thesis: for i, j being Nat st len p = 0 & len p = i + j holds
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
let i, j be Nat; ::_thesis: ( len p = 0 & len p = i + j implies ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 ) )
assume that
A14: len p = 0 and
A15: len p = i + j ; ::_thesis: ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
p = {} by A14;
then A16: p = {} ^ {} ;
len {} = i by A14, A15;
hence ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 ) by A15, A16; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A13, A1);
hence ( len p = n + k implies ex q1, q2 being XFinSequence st
( len q1 = n & len q2 = k & p = q1 ^ q2 ) ) ; ::_thesis: verum
end;
theorem :: AFINSQ_1:62
for x, y being set
for p, q being XFinSequence st <%x%> ^ p = <%y%> ^ q holds
( x = y & p = q )
proof
let x, y be set ; ::_thesis: for p, q being XFinSequence st <%x%> ^ p = <%y%> ^ q holds
( x = y & p = q )
let p, q be XFinSequence; ::_thesis: ( <%x%> ^ p = <%y%> ^ q implies ( x = y & p = q ) )
assume A1: <%x%> ^ p = <%y%> ^ q ; ::_thesis: ( x = y & p = q )
(<%x%> ^ p) . 0 = x by Th35;
then x = y by A1, Th35;
hence ( x = y & p = q ) by A1, Th28; ::_thesis: verum
end;
definition
let D be set ;
let q be FinSequence of D;
func FS2XFS q -> XFinSequence of D means :Def8: :: AFINSQ_1:def 8
( len it = len q & ( for i being Nat st i < len q holds
q . (i + 1) = it . i ) );
existence
ex b1 being XFinSequence of D st
( len b1 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b1 . i ) )
proof
deffunc H1( Nat) -> set = q . ($1 + 1);
ex p being XFinSequence st
( len p = len q & ( for k being Nat st k in len q holds
p . k = H1(k) ) ) from AFINSQ_1:sch_2();
then consider p being XFinSequence such that
A1: len p = len q and
A2: for k being Nat st k in len q holds
p . k = H1(k) ;
rng p c= D
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in D )
A3: rng q c= D by FINSEQ_1:def_4;
assume y in rng p ; ::_thesis: y in D
then consider x being set such that
A4: x in dom p and
A5: y = p . x by FUNCT_1:def_3;
reconsider nx = x as Element of NAT by A4;
nx < len q by A1, A4, NAT_1:44;
then A6: nx + 1 <= len q by NAT_1:13;
0 + 1 <= nx + 1 by NAT_1:13;
then nx + 1 in Seg (len q) by A6, FINSEQ_1:1;
then nx + 1 in dom q by FINSEQ_1:def_3;
then A7: q . (nx + 1) in rng q by FUNCT_1:def_3;
p . nx = q . (nx + 1) by A1, A2, A4;
hence y in D by A5, A7, A3; ::_thesis: verum
end;
then A8: p is XFinSequence of D by RELAT_1:def_19;
for i being Nat st i < len q holds
q . (i + 1) = p . i
proof
let i be Nat; ::_thesis: ( i < len q implies q . (i + 1) = p . i )
assume i < len q ; ::_thesis: q . (i + 1) = p . i
then ( i in NAT & i in len q ) by NAT_1:44, ORDINAL1:def_12;
hence q . (i + 1) = p . i by A2; ::_thesis: verum
end;
hence ex b1 being XFinSequence of D st
( len b1 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b1 . i ) ) by A1, A8; ::_thesis: verum
end;
uniqueness
for b1, b2 being XFinSequence of D st len b1 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b1 . i ) & len b2 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b2 . i ) holds
b1 = b2
proof
thus for p1, p2 being XFinSequence of D st len p1 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = p1 . i ) & len p2 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = p2 . i ) holds
p1 = p2 ::_thesis: verum
proof
let p1, p2 be XFinSequence of D; ::_thesis: ( len p1 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = p1 . i ) & len p2 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = p2 . i ) implies p1 = p2 )
assume that
A9: len p1 = len q and
A10: for i being Nat st i < len q holds
q . (i + 1) = p1 . i and
A11: len p2 = len q and
A12: for i being Nat st i < len q holds
q . (i + 1) = p2 . i ; ::_thesis: p1 = p2
for i being Nat st i < len p1 holds
p1 . i = p2 . i
proof
let i be Nat; ::_thesis: ( i < len p1 implies p1 . i = p2 . i )
assume A13: i < len p1 ; ::_thesis: p1 . i = p2 . i
then q . (i + 1) = p1 . i by A9, A10;
hence p1 . i = p2 . i by A9, A12, A13; ::_thesis: verum
end;
hence p1 = p2 by A9, A11, Th9; ::_thesis: verum
end;
end;
end;
:: deftheorem Def8 defines FS2XFS AFINSQ_1:def_8_:_
for D being set
for q being FinSequence of D
for b3 being XFinSequence of D holds
( b3 = FS2XFS q iff ( len b3 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b3 . i ) ) );
definition
let D be set ;
let q be XFinSequence of D;
func XFS2FS q -> FinSequence of D means :: AFINSQ_1:def 9
( len it = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = it . i ) );
existence
ex b1 being FinSequence of D st
( len b1 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b1 . i ) )
proof
deffunc H1( Nat) -> set = q . ($1 -' 1);
ex p being FinSequence st
( len p = len q & ( for k being Nat st k in dom p holds
p . k = H1(k) ) ) from FINSEQ_1:sch_2();
then consider p being FinSequence such that
A1: len p = len q and
A2: for k being Nat st k in dom p holds
p . k = H1(k) ;
rng p c= D
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in D )
A3: rng q c= D by RELAT_1:def_19;
assume y in rng p ; ::_thesis: y in D
then consider x being set such that
A4: x in dom p and
A5: y = p . x by FUNCT_1:def_3;
reconsider nx = x as Element of NAT by A4;
A6: nx in Seg (len q) by A1, A4, FINSEQ_1:def_3;
then 1 <= nx by FINSEQ_1:1;
then nx - 1 >= 0 by XREAL_1:48;
then A7: nx - 1 = nx -' 1 by XREAL_0:def_2;
A8: nx -' 1 < (nx -' 1) + 1 by NAT_1:13;
nx <= len q by A6, FINSEQ_1:1;
then nx -' 1 < len q by A7, A8, XXREAL_0:2;
then nx -' 1 in dom q by NAT_1:44;
then A9: q . (nx -' 1) in rng q by FUNCT_1:def_3;
p . nx = q . (nx -' 1) by A2, A4;
hence y in D by A5, A9, A3; ::_thesis: verum
end;
then A10: p is FinSequence of D by FINSEQ_1:def_4;
A11: dom p = Seg (len q) by A1, FINSEQ_1:def_3;
for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = p . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len q implies q . (i -' 1) = p . i )
assume ( 1 <= i & i <= len q ) ; ::_thesis: q . (i -' 1) = p . i
then i in Seg (len q) by FINSEQ_1:1;
hence q . (i -' 1) = p . i by A2, A11; ::_thesis: verum
end;
hence ex b1 being FinSequence of D st
( len b1 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b1 . i ) ) by A1, A10; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of D st len b1 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b1 . i ) & len b2 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b2 . i ) holds
b1 = b2
proof
thus for p1, p2 being FinSequence of D st len p1 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = p1 . i ) & len p2 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = p2 . i ) holds
p1 = p2 ::_thesis: verum
proof
let p1, p2 be FinSequence of D; ::_thesis: ( len p1 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = p1 . i ) & len p2 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = p2 . i ) implies p1 = p2 )
assume that
A12: len p1 = len q and
A13: for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = p1 . i and
A14: len p2 = len q and
A15: for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = p2 . i ; ::_thesis: p1 = p2
for i being Nat st 1 <= i & i <= len p1 holds
p1 . i = p2 . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len p1 implies p1 . i = p2 . i )
assume A16: ( 1 <= i & i <= len p1 ) ; ::_thesis: p1 . i = p2 . i
then q . (i -' 1) = p1 . i by A12, A13;
hence p1 . i = p2 . i by A12, A15, A16; ::_thesis: verum
end;
hence p1 = p2 by A12, A14, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;
:: deftheorem defines XFS2FS AFINSQ_1:def_9_:_
for D being set
for q being XFinSequence of D
for b3 being FinSequence of D holds
( b3 = XFS2FS q iff ( len b3 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b3 . i ) ) );
theorem :: AFINSQ_1:63
for D being set
for n being Nat
for r being set st r in D holds
n --> r is XFinSequence of D ;
definition
let D be non empty set ;
let q be FinSequence of D;
let n be Nat;
assume that
A1: n > len q and
A2: NAT c= D ;
func FS2XFS* (q,n) -> non empty XFinSequence of D means :: AFINSQ_1:def 10
( len q = it . 0 & len it = n & ( for i being Nat st 1 <= i & i <= len q holds
it . i = q . i ) & ( for j being Nat st len q < j & j < n holds
it . j = 0 ) );
existence
ex b1 being non empty XFinSequence of D st
( len q = b1 . 0 & len b1 = n & ( for i being Nat st 1 <= i & i <= len q holds
b1 . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b1 . j = 0 ) )
proof
len q in NAT ;
then reconsider x = len q as Element of D by A2;
0 in NAT ;
then reconsider r = 0 as Element of D by A2;
reconsider q5 = ((n -' (len q)) -' 1) --> r as XFinSequence of D ;
<%x%> ^ (FS2XFS q) <> {} by Th30;
then reconsider p0 = (<%x%> ^ (FS2XFS q)) ^ q5 as non empty XFinSequence of D by Th30;
A3: 0 in dom <%x%> by NAT_1:44;
A4: len <%x%> = 1 by Def4;
0 in (len <%x%>) + (len (FS2XFS q)) by NAT_1:44;
then 0 in len (<%x%> ^ (FS2XFS q)) by Def3;
then A5: p0 . 0 = (<%x%> ^ (FS2XFS q)) . 0 by Def3
.= <%x%> . 0 by A3, Def3
.= x by Def4 ;
A6: for i being Nat st 1 <= i & i <= len q holds
p0 . i = q . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len q implies p0 . i = q . i )
assume that
A7: 1 <= i and
A8: i <= len q ; ::_thesis: p0 . i = q . i
i - 1 >= 0 by A7, XREAL_1:48;
then A9: i -' 1 = i - 1 by XREAL_0:def_2;
i < i + 1 by NAT_1:13;
then i - 1 < (i + 1) - 1 by XREAL_1:9;
then A10: i -' 1 < len q by A8, A9, XXREAL_0:2;
then i -' 1 in len q by NAT_1:44;
then A11: i -' 1 in len (FS2XFS q) by Def8;
i < 1 + (len q) by A8, NAT_1:13;
then i < (len <%x%>) + (len (FS2XFS q)) by A4, Def8;
then i in (len <%x%>) + (len (FS2XFS q)) by NAT_1:44;
then i in len (<%x%> ^ (FS2XFS q)) by Def3;
then p0 . i = (<%x%> ^ (FS2XFS q)) . (1 + (i -' 1)) by A9, Def3
.= (FS2XFS q) . (i -' 1) by A4, A11, Def3
.= q . ((i -' 1) + 1) by A10, Def8
.= q . i by A9 ;
hence p0 . i = q . i ; ::_thesis: verum
end;
A12: n - (len q) > 0 by A1, XREAL_1:50;
then A13: n -' (len q) = n - (len q) by XREAL_0:def_2;
then n -' (len q) >= 0 + 1 by A12, NAT_1:13;
then A14: (n -' (len q)) - 1 >= 0 by XREAL_1:48;
A15: len q5 = (n -' (len q)) -' 1 by FUNCOP_1:13;
A16: for j being Nat st len q < j & j < n holds
p0 . j = 0
proof
let j be Nat; ::_thesis: ( len q < j & j < n implies p0 . j = 0 )
assume that
A17: len q < j and
A18: j < n ; ::_thesis: p0 . j = 0
A19: len (<%x%> ^ (FS2XFS q)) = (len <%x%>) + (len (FS2XFS q)) by Def3
.= 1 + (len q) by A4, Def8 ;
len q < n by A17, A18, XXREAL_0:2;
then A20: n - (len q) > 0 by XREAL_1:50;
then A21: n -' (len q) = n - (len q) by XREAL_0:def_2;
then n - (len q) >= 0 + 1 by A20, NAT_1:13;
then (n -' (len q)) - 1 >= 0 by A21, XREAL_1:48;
then A22: (n -' (len q)) -' 1 = n - ((len q) + 1) by A21, XREAL_0:def_2;
1 + (len q) <= j by A17, NAT_1:13;
then j - (1 + (len q)) >= 0 by XREAL_1:48;
then A23: j -' (1 + (len q)) = j - (1 + (len q)) by XREAL_0:def_2;
j - ((len q) + 1) < n - ((len q) + 1) by A18, XREAL_1:9;
then A24: j -' (len (<%x%> ^ (FS2XFS q))) in (n -' (len q)) -' 1 by A19, A23, A22, NAT_1:44;
j = (len (<%x%> ^ (FS2XFS q))) + (j -' (len (<%x%> ^ (FS2XFS q)))) by A19, A23;
then p0 . j = q5 . (j -' (len (<%x%> ^ (FS2XFS q)))) by A15, A24, Def3
.= 0 by A24, FUNCOP_1:7 ;
hence p0 . j = 0 ; ::_thesis: verum
end;
len p0 = (len (<%x%> ^ (FS2XFS q))) + (len q5) by Def3
.= ((len <%x%>) + (len (FS2XFS q))) + (len q5) by Def3
.= (1 + (len (FS2XFS q))) + (len q5) by Th33
.= (1 + (len q)) + (len q5) by Def8
.= (1 + (len q)) + ((n -' (len q)) -' 1) by FUNCOP_1:13
.= (n - ((len q) + 1)) + ((len q) + 1) by A13, A14, XREAL_0:def_2
.= n ;
hence ex b1 being non empty XFinSequence of D st
( len q = b1 . 0 & len b1 = n & ( for i being Nat st 1 <= i & i <= len q holds
b1 . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b1 . j = 0 ) ) by A5, A6, A16; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty XFinSequence of D st len q = b1 . 0 & len b1 = n & ( for i being Nat st 1 <= i & i <= len q holds
b1 . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b1 . j = 0 ) & len q = b2 . 0 & len b2 = n & ( for i being Nat st 1 <= i & i <= len q holds
b2 . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b2 . j = 0 ) holds
b1 = b2
proof
let p1, p2 be non empty XFinSequence of D; ::_thesis: ( len q = p1 . 0 & len p1 = n & ( for i being Nat st 1 <= i & i <= len q holds
p1 . i = q . i ) & ( for j being Nat st len q < j & j < n holds
p1 . j = 0 ) & len q = p2 . 0 & len p2 = n & ( for i being Nat st 1 <= i & i <= len q holds
p2 . i = q . i ) & ( for j being Nat st len q < j & j < n holds
p2 . j = 0 ) implies p1 = p2 )
assume that
A25: len q = p1 . 0 and
A26: len p1 = n and
A27: for i being Nat st 1 <= i & i <= len q holds
p1 . i = q . i and
A28: for j being Nat st len q < j & j < n holds
p1 . j = 0 and
A29: len q = p2 . 0 and
A30: len p2 = n and
A31: for i being Nat st 1 <= i & i <= len q holds
p2 . i = q . i and
A32: for j being Nat st len q < j & j < n holds
p2 . j = 0 ; ::_thesis: p1 = p2
for i being Nat st i < n holds
p1 . i = p2 . i
proof
let i be Nat; ::_thesis: ( i < n implies p1 . i = p2 . i )
assume i < n ; ::_thesis: p1 . i = p2 . i
then A33: ( i < 0 + 1 or ( 1 <= i & i <= len q ) or ( len q < i & i < n ) ) ;
now__::_thesis:_(_(_i_=_0_&_p1_._i_=_p2_._i_)_or_(_1_<=_i_&_i_<=_len_q_&_p1_._i_=_p2_._i_)_or_(_len_q_<_i_&_i_<_n_&_p1_._i_=_p2_._i_)_)
percases ( i = 0 or ( 1 <= i & i <= len q ) or ( len q < i & i < n ) ) by A33, NAT_1:13;
case i = 0 ; ::_thesis: p1 . i = p2 . i
hence p1 . i = p2 . i by A25, A29; ::_thesis: verum
end;
caseA34: ( 1 <= i & i <= len q ) ; ::_thesis: p1 . i = p2 . i
then p1 . i = q . i by A27;
hence p1 . i = p2 . i by A31, A34; ::_thesis: verum
end;
caseA35: ( len q < i & i < n ) ; ::_thesis: p1 . i = p2 . i
then p1 . i = 0 by A28;
hence p1 . i = p2 . i by A32, A35; ::_thesis: verum
end;
end;
end;
hence p1 . i = p2 . i ; ::_thesis: verum
end;
hence p1 = p2 by A26, A30, Th9; ::_thesis: verum
end;
end;
:: deftheorem defines FS2XFS* AFINSQ_1:def_10_:_
for D being non empty set
for q being FinSequence of D
for n being Nat st n > len q & NAT c= D holds
for b4 being non empty XFinSequence of D holds
( b4 = FS2XFS* (q,n) iff ( len q = b4 . 0 & len b4 = n & ( for i being Nat st 1 <= i & i <= len q holds
b4 . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b4 . j = 0 ) ) );
definition
let D be non empty set ;
let p be XFinSequence of D;
assume that
A1: p . 0 is Nat and
A2: p . 0 in len p ;
func XFS2FS* p -> FinSequence of D means :Def11: :: AFINSQ_1:def 11
for m being Nat st m = p . 0 holds
( len it = m & ( for i being Nat st 1 <= i & i <= m holds
it . i = p . i ) );
existence
ex b1 being FinSequence of D st
for m being Nat st m = p . 0 holds
( len b1 = m & ( for i being Nat st 1 <= i & i <= m holds
b1 . i = p . i ) )
proof
reconsider m0 = p . 0 as Element of NAT by A1, ORDINAL1:def_12;
deffunc H1( set ) -> set = p . $1;
ex q being FinSequence st
( len q = m0 & ( for k being Nat st k in dom q holds
q . k = H1(k) ) ) from FINSEQ_1:sch_2();
then consider q being FinSequence such that
A3: len q = m0 and
A4: for k being Nat st k in dom q holds
q . k = H1(k) ;
rng q c= D
proof
A5: m0 < len p by A2, NAT_1:44;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng q or y in D )
assume y in rng q ; ::_thesis: y in D
then consider x being set such that
A6: x in dom q and
A7: y = q . x by FUNCT_1:def_3;
reconsider k0 = x as Element of NAT by A6;
k0 in Seg m0 by A3, A6, FINSEQ_1:def_3;
then k0 <= m0 by FINSEQ_1:1;
then k0 < len p by A5, XXREAL_0:2;
then A8: k0 in dom p by NAT_1:44;
y = p . k0 by A4, A6, A7;
then ( rng p c= D & y in rng p ) by A8, FUNCT_1:def_3, RELAT_1:def_19;
hence y in D ; ::_thesis: verum
end;
then reconsider q0 = q as FinSequence of D by FINSEQ_1:def_4;
A9: dom q = Seg m0 by A3, FINSEQ_1:def_3;
for m being Nat st m = p . 0 holds
( len q0 = m & ( for i being Nat st 1 <= i & i <= m holds
q0 . i = p . i ) )
proof
let m be Nat; ::_thesis: ( m = p . 0 implies ( len q0 = m & ( for i being Nat st 1 <= i & i <= m holds
q0 . i = p . i ) ) )
A10: for i being Nat st 1 <= i & i <= m0 holds
q0 . i = p . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= m0 implies q0 . i = p . i )
assume ( 1 <= i & i <= m0 ) ; ::_thesis: q0 . i = p . i
then i in Seg m0 by FINSEQ_1:1;
hence q0 . i = p . i by A4, A9; ::_thesis: verum
end;
assume m = p . 0 ; ::_thesis: ( len q0 = m & ( for i being Nat st 1 <= i & i <= m holds
q0 . i = p . i ) )
hence ( len q0 = m & ( for i being Nat st 1 <= i & i <= m holds
q0 . i = p . i ) ) by A3, A10; ::_thesis: verum
end;
hence ex b1 being FinSequence of D st
for m being Nat st m = p . 0 holds
( len b1 = m & ( for i being Nat st 1 <= i & i <= m holds
b1 . i = p . i ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of D st ( for m being Nat st m = p . 0 holds
( len b1 = m & ( for i being Nat st 1 <= i & i <= m holds
b1 . i = p . i ) ) ) & ( for m being Nat st m = p . 0 holds
( len b2 = m & ( for i being Nat st 1 <= i & i <= m holds
b2 . i = p . i ) ) ) holds
b1 = b2
proof
reconsider m2 = p . 0 as Nat by A1;
let g1, g2 be FinSequence of D; ::_thesis: ( ( for m being Nat st m = p . 0 holds
( len g1 = m & ( for i being Nat st 1 <= i & i <= m holds
g1 . i = p . i ) ) ) & ( for m being Nat st m = p . 0 holds
( len g2 = m & ( for i being Nat st 1 <= i & i <= m holds
g2 . i = p . i ) ) ) implies g1 = g2 )
assume that
A11: for m being Nat st m = p . 0 holds
( len g1 = m & ( for i being Nat st 1 <= i & i <= m holds
g1 . i = p . i ) ) and
A12: for m being Nat st m = p . 0 holds
( len g2 = m & ( for i being Nat st 1 <= i & i <= m holds
g2 . i = p . i ) ) ; ::_thesis: g1 = g2
A13: len g1 = m2 by A11;
A14: for i being Nat st 1 <= i & i <= len g1 holds
g1 . i = g2 . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len g1 implies g1 . i = g2 . i )
assume A15: ( 1 <= i & i <= len g1 ) ; ::_thesis: g1 . i = g2 . i
then g1 . i = p . i by A11, A13;
hence g1 . i = g2 . i by A12, A13, A15; ::_thesis: verum
end;
len g2 = m2 by A12;
hence g1 = g2 by A11, A14, FINSEQ_1:14; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines XFS2FS* AFINSQ_1:def_11_:_
for D being non empty set
for p being XFinSequence of D st p . 0 is Nat & p . 0 in len p holds
for b3 being FinSequence of D holds
( b3 = XFS2FS* p iff for m being Nat st m = p . 0 holds
( len b3 = m & ( for i being Nat st 1 <= i & i <= m holds
b3 . i = p . i ) ) );
theorem :: AFINSQ_1:64
for D being non empty set
for p being XFinSequence of D st p . 0 = 0 & 0 < len p holds
XFS2FS* p = {}
proof
let D be non empty set ; ::_thesis: for p being XFinSequence of D st p . 0 = 0 & 0 < len p holds
XFS2FS* p = {}
let p be XFinSequence of D; ::_thesis: ( p . 0 = 0 & 0 < len p implies XFS2FS* p = {} )
assume that
A1: p . 0 = 0 and
A2: 0 < len p ; ::_thesis: XFS2FS* p = {}
set q = XFS2FS* p;
0 in len p by A2, NAT_1:44;
then len (XFS2FS* p) = 0 by A1, Def11;
hence XFS2FS* p = {} ; ::_thesis: verum
end;
definition
let F be Function;
attrF is initial means :Def12: :: AFINSQ_1:def 12
for m, n being Nat st n in dom F & m < n holds
m in dom F;
end;
:: deftheorem Def12 defines initial AFINSQ_1:def_12_:_
for F being Function holds
( F is initial iff for m, n being Nat st n in dom F & m < n holds
m in dom F );
registration
cluster Relation-like Function-like empty -> initial for set ;
coherence
for b1 being Function st b1 is empty holds
b1 is initial
proof
let F be Function; ::_thesis: ( F is empty implies F is initial )
assume A1: F is empty ; ::_thesis: F is initial
let n be Nat; :: according to AFINSQ_1:def_12 ::_thesis: for n being Nat st n in dom F & n < n holds
n in dom F
thus for n being Nat st n in dom F & n < n holds
n in dom F by A1; ::_thesis: verum
end;
end;
registration
cluster Relation-like T-Sequence-like Function-like finite -> initial for set ;
coherence
for b1 being XFinSequence holds b1 is initial
proof
let p be XFinSequence; ::_thesis: p is initial
let m, n be Nat; :: according to AFINSQ_1:def_12 ::_thesis: ( n in dom p & m < n implies m in dom p )
assume A1: n in dom p ; ::_thesis: ( not m < n or m in dom p )
assume m < n ; ::_thesis: m in dom p
then m in n by NAT_1:44;
hence m in dom p by A1, ORDINAL1:10; ::_thesis: verum
end;
end;
registration
cluster Relation-like T-Sequence-like Function-like finite -> NAT -defined for set ;
coherence
for b1 being XFinSequence holds b1 is NAT -defined
proof
let f be XFinSequence; ::_thesis: f is NAT -defined
thus dom f c= NAT ; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;
theorem Th65: :: AFINSQ_1:65
for F being NAT -defined non empty initial Function holds 0 in dom F
proof
let F be NAT -defined non empty initial Function; ::_thesis: 0 in dom F
consider x being set such that
A1: x in dom F by XBOOLE_0:def_1;
dom F c= NAT by RELAT_1:def_18;
then reconsider x = x as Element of NAT by A1;
( x = 0 or 0 < x ) ;
hence 0 in dom F by A1, Def12; ::_thesis: verum
end;
registration
cluster Relation-like NAT -defined Function-like finite initial -> T-Sequence-like for set ;
coherence
for b1 being Function st b1 is initial & b1 is finite & b1 is NAT -defined holds
b1 is T-Sequence-like
proof
let F be Function; ::_thesis: ( F is initial & F is finite & F is NAT -defined implies F is T-Sequence-like )
assume A1: ( F is initial & F is finite & F is NAT -defined ) ; ::_thesis: F is T-Sequence-like
then A2: dom F c= NAT by RELAT_1:def_18;
thus dom F is epsilon-transitive :: according to ORDINAL1:def_4,ORDINAL1:def_7 ::_thesis: dom F is epsilon-connected
proof
let x be set ; :: according to ORDINAL1:def_2 ::_thesis: ( not x in dom F or x c= dom F )
assume A3: x in dom F ; ::_thesis: x c= dom F
then reconsider i = x as Nat by A1;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x or y in dom F )
assume A4: y in x ; ::_thesis: y in dom F
reconsider j = y as Nat by A4, A3, A2;
j < i by A4, NAT_1:44;
hence y in dom F by A1, A3, Def12; ::_thesis: verum
end;
let x be set ; :: according to ORDINAL1:def_3 ::_thesis: for b1 being set holds
( not x in dom F or not b1 in dom F or x in b1 or x = b1 or b1 in x )
let y be set ; ::_thesis: ( not x in dom F or not y in dom F or x in y or x = y or y in x )
assume ( x in dom F & y in dom F ) ; ::_thesis: ( x in y or x = y or y in x )
then reconsider x = x, y = y as Ordinal by A1;
( x in y or x = y or y in x ) by ORDINAL1:14;
hence ( x in y or x = y or y in x ) ; ::_thesis: verum
end;
end;
theorem :: AFINSQ_1:66
for F being NAT -defined finite initial Function
for n being Nat holds
( n in dom F iff n < card F ) by NAT_1:44;
theorem :: AFINSQ_1:67
for F being NAT -defined initial Function
for G being NAT -defined Function st dom F = dom G holds
G is initial
proof
let F be NAT -defined initial Function; ::_thesis: for G being NAT -defined Function st dom F = dom G holds
G is initial
let G be NAT -defined Function; ::_thesis: ( dom F = dom G implies G is initial )
assume dom F = dom G ; ::_thesis: G is initial
hence for m, l being Nat st l in dom G & m < l holds
m in dom G by Def12; :: according to AFINSQ_1:def_12 ::_thesis: verum
end;
theorem :: AFINSQ_1:68
for F being NAT -defined finite initial Function holds dom F = { k where k is Element of NAT : k < card F }
proof
let F be NAT -defined finite initial Function; ::_thesis: dom F = { k where k is Element of NAT : k < card F }
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { k where k is Element of NAT : k < card F } c= dom F
let x be set ; ::_thesis: ( x in dom F implies x in { k where k is Element of NAT : k < card F } )
assume A1: x in dom F ; ::_thesis: x in { k where k is Element of NAT : k < card F }
then reconsider f = x as Element of NAT ;
f < card F by A1, NAT_1:44;
hence x in { k where k is Element of NAT : k < card F } ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : k < card F } or x in dom F )
assume x in { k where k is Element of NAT : k < card F } ; ::_thesis: x in dom F
then ex k being Element of NAT st
( x = k & k < card F ) ;
hence x in dom F by NAT_1:44; ::_thesis: verum
end;
theorem :: AFINSQ_1:69
for F being NAT -defined non empty finite initial Function
for G being NAT -defined non empty finite Function st F c= G & LastLoc F = LastLoc G holds
F = G
proof
let F be NAT -defined non empty finite initial Function; ::_thesis: for G being NAT -defined non empty finite Function st F c= G & LastLoc F = LastLoc G holds
F = G
let G be NAT -defined non empty finite Function; ::_thesis: ( F c= G & LastLoc F = LastLoc G implies F = G )
assume that
A1: F c= G and
A2: LastLoc F = LastLoc G ; ::_thesis: F = G
dom F = dom G
proof
thus dom F c= dom G by A1, GRFUNC_1:2; :: according to XBOOLE_0:def_10 ::_thesis: dom G c= dom F
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom G or x in dom F )
assume A3: x in dom G ; ::_thesis: x in dom F
dom G c= NAT by RELAT_1:def_18;
then reconsider x = x as Element of NAT by A3;
A4: LastLoc F in dom F by VALUED_1:30;
x <= LastLoc F by A2, A3, VALUED_1:32;
then ( x < LastLoc F or x = LastLoc F ) by XXREAL_0:1;
hence x in dom F by A4, Def12; ::_thesis: verum
end;
hence F = G by A1, GRFUNC_1:3; ::_thesis: verum
end;
theorem :: AFINSQ_1:70
for F being NAT -defined non empty finite initial Function holds LastLoc F = (card F) -' 1
proof
let F be NAT -defined non empty finite initial Function; ::_thesis: LastLoc F = (card F) -' 1
consider k being Nat such that
A1: LastLoc F = k ;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
LastLoc F in dom F by VALUED_1:30;
then k < card F by A1, NAT_1:44;
then A2: k <= (card F) -' 1 by NAT_D:49;
percases ( k < (card F) -' 1 or k = (card F) -' 1 ) by A2, XXREAL_0:1;
suppose k < (card F) -' 1 ; ::_thesis: LastLoc F = (card F) -' 1
then k + 1 < ((card F) -' 1) + 1 by XREAL_1:6;
then k + 1 < card F by NAT_1:14, XREAL_1:235;
then k + 1 in dom F by NAT_1:44;
then A3: k + 1 <= k by A1, VALUED_1:32;
k <= k + 1 by NAT_1:11;
then k + 0 = k + 1 by A3, XXREAL_0:1;
hence LastLoc F = (card F) -' 1 ; ::_thesis: verum
end;
suppose k = (card F) -' 1 ; ::_thesis: LastLoc F = (card F) -' 1
hence LastLoc F = (card F) -' 1 by A1; ::_thesis: verum
end;
end;
end;
theorem :: AFINSQ_1:71
for F being NAT -defined non empty finite initial Function holds FirstLoc F = 0 by Th65, VALUED_1:35;
registration
let F be NAT -defined non empty finite initial Function;
cluster CutLastLoc F -> initial ;
coherence
CutLastLoc F is initial
proof
set G = CutLastLoc F;
percases ( CutLastLoc F is empty or not CutLastLoc F is empty ) ;
suppose CutLastLoc F is empty ; ::_thesis: CutLastLoc F is initial
then reconsider H = CutLastLoc F as empty finite Function ;
H is initial ;
hence CutLastLoc F is initial ; ::_thesis: verum
end;
suppose not CutLastLoc F is empty ; ::_thesis: CutLastLoc F is initial
then reconsider G = CutLastLoc F as non empty finite Function ;
G is initial
proof
let m, l be Nat; :: according to AFINSQ_1:def_12 ::_thesis: ( l in dom G & m < l implies m in dom G )
assume that
A1: l in dom G and
A2: m < l ; ::_thesis: m in dom G
set M = dom F;
reconsider R = {[(LastLoc F),(F . (LastLoc F))]} as Relation ;
R = (LastLoc F) .--> (F . (LastLoc F)) by FUNCT_4:82;
then A3: dom R = {(LastLoc F)} by FUNCOP_1:13;
then A4: (dom F) \ (dom R) = dom G by VALUED_1:36;
then l in dom F by A1, XBOOLE_0:def_5;
then A5: m in dom F by A2, Def12;
l in dom F by A4, A1, XBOOLE_0:def_5;
then m <> LastLoc F by A2, XXREAL_2:def_8;
then not m in {(LastLoc F)} by TARSKI:def_1;
hence m in dom G by A3, A4, A5, XBOOLE_0:def_5; ::_thesis: verum
end;
hence CutLastLoc F is initial ; ::_thesis: verum
end;
end;
end;
end;
theorem :: AFINSQ_1:72
for I being NAT -defined finite initial Function
for J being Function holds dom I misses dom (Shift (J,(card I)))
proof
let I be NAT -defined finite initial Function; ::_thesis: for J being Function holds dom I misses dom (Shift (J,(card I)))
let J be Function; ::_thesis: dom I misses dom (Shift (J,(card I)))
assume A1: dom I meets dom (Shift (J,(card I))) ; ::_thesis: contradiction
dom (Shift (J,(card I))) = { (l + (card I)) where l is Element of NAT : l in dom J } by VALUED_1:def_12;
then consider x being set such that
A2: x in dom I and
A3: x in { (l + (card I)) where l is Element of NAT : l in dom J } by A1, XBOOLE_0:3;
consider l being Element of NAT such that
A4: x = l + (card I) and
l in dom J by A3;
l + (card I) < card I by A2, A4, NAT_1:44;
hence contradiction by NAT_1:11; ::_thesis: verum
end;
theorem :: AFINSQ_1:73
for p being XFinSequence
for m being Nat st not m in dom p holds
not succ m in dom p
proof
let p be XFinSequence; ::_thesis: for m being Nat st not m in dom p holds
not succ m in dom p
let m be Nat; ::_thesis: ( not m in dom p implies not succ m in dom p )
assume not m in dom p ; ::_thesis: not succ m in dom p
then A1: m >= card p by NAT_1:44;
m + 1 >= m by NAT_1:11;
then m + 1 >= card p by A1, XXREAL_0:2;
hence not succ m in dom p by NAT_1:44; ::_thesis: verum
end;
registration
let D be set ;
clusterD ^omega -> functional ;
coherence
D ^omega is functional
proof
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in D ^omega or x is set )
assume x in D ^omega ; ::_thesis: x is set
hence x is Function by Def7; ::_thesis: verum
end;
end;
registration
let D be set ;
cluster -> T-Sequence-like finite for Element of D ^omega ;
coherence
for b1 being Element of D ^omega holds
( b1 is finite & b1 is T-Sequence-like ) by Def7;
end;
definition
let D be set ;
let f be XFinSequence of D;
func Down f -> Element of D ^omega equals :: AFINSQ_1:def 13
f;
coherence
f is Element of D ^omega by Def7;
end;
:: deftheorem defines Down AFINSQ_1:def_13_:_
for D being set
for f being XFinSequence of D holds Down f = f;
definition
let D be set ;
let f be XFinSequence of D;
let g be Element of D ^omega ;
:: original: ^
redefine funcf ^ g -> Element of D ^omega ;
coherence
f ^ g is Element of D ^omega
proof
reconsider g = g as XFinSequence of D by Def7;
f ^ g is XFinSequence of D ;
hence f ^ g is Element of D ^omega by Def7; ::_thesis: verum
end;
end;
definition
let D be set ;
let f, g be Element of D ^omega ;
:: original: ^
redefine funcf ^ g -> Element of D ^omega ;
coherence
f ^ g is Element of D ^omega
proof
reconsider f = f, g = g as XFinSequence of D by Def7;
f ^ g is XFinSequence of D ;
hence f ^ g is Element of D ^omega by Def7; ::_thesis: verum
end;
end;
theorem Th74: :: AFINSQ_1:74
for p, q being XFinSequence holds p c= p ^ q
proof
let p, q be XFinSequence; ::_thesis: p c= p ^ q
A1: dom p c= dom (p ^ q) by Th21;
for x being set st x in dom p holds
(p ^ q) . x = p . x by Def3;
hence p c= p ^ q by A1, GRFUNC_1:2; ::_thesis: verum
end;
theorem Th75: :: AFINSQ_1:75
for x being set
for p being XFinSequence holds len (p ^ <%x%>) = (len p) + 1
proof
let x be set ; ::_thesis: for p being XFinSequence holds len (p ^ <%x%>) = (len p) + 1
let p be XFinSequence; ::_thesis: len (p ^ <%x%>) = (len p) + 1
thus len (p ^ <%x%>) = (len p) + (len <%x%>) by Def3
.= (len p) + 1 by Th33 ; ::_thesis: verum
end;
theorem :: AFINSQ_1:76
for x, y being set holds <%x,y%> = (0,1) --> (x,y)
proof
let x, y be set ; ::_thesis: <%x,y%> = (0,1) --> (x,y)
A1: dom <%x,y%> = len <%x,y%>
.= {0,1} by Th38, CARD_1:50 ;
A2: <%x,y%> . 0 = x by Th38;
<%x,y%> . 1 = y by Th38;
hence <%x,y%> = (0,1) --> (x,y) by A1, A2, FUNCT_4:66; ::_thesis: verum
end;
theorem Th77: :: AFINSQ_1:77
for p, q being XFinSequence holds p ^ q = p +* (Shift (q,(card p)))
proof
let p, q be XFinSequence; ::_thesis: p ^ q = p +* (Shift (q,(card p)))
A1: dom (Shift (q,(card p))) = { (M + (card p)) where M is Element of NAT : M in dom q } by VALUED_1:def_12;
for x being set holds
( x in dom (p ^ q) iff ( x in dom p or x in dom (Shift (q,(card p))) ) )
proof
let x be set ; ::_thesis: ( x in dom (p ^ q) iff ( x in dom p or x in dom (Shift (q,(card p))) ) )
thus ( not x in dom (p ^ q) or x in dom p or x in dom (Shift (q,(card p))) ) ::_thesis: ( ( x in dom p or x in dom (Shift (q,(card p))) ) implies x in dom (p ^ q) )
proof
assume A2: x in dom (p ^ q) ; ::_thesis: ( x in dom p or x in dom (Shift (q,(card p))) )
then reconsider k = x as Nat ;
percases ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by A2, Th20;
suppose k in dom p ; ::_thesis: ( x in dom p or x in dom (Shift (q,(card p))) )
hence ( x in dom p or x in dom (Shift (q,(card p))) ) ; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom q & k = (len p) + n ) ; ::_thesis: ( x in dom p or x in dom (Shift (q,(card p))) )
hence ( x in dom p or x in dom (Shift (q,(card p))) ) by A1; ::_thesis: verum
end;
end;
end;
assume A3: ( x in dom p or x in dom (Shift (q,(card p))) ) ; ::_thesis: x in dom (p ^ q)
percases ( x in dom p or x in dom (Shift (q,(card p))) ) by A3;
supposeA4: x in dom p ; ::_thesis: x in dom (p ^ q)
dom p c= dom (p ^ q) by Th21;
hence x in dom (p ^ q) by A4; ::_thesis: verum
end;
suppose x in dom (Shift (q,(card p))) ; ::_thesis: x in dom (p ^ q)
then ex M being Element of NAT st
( x = M + (card p) & M in dom q ) by A1;
hence x in dom (p ^ q) by Th23; ::_thesis: verum
end;
end;
end;
then A5: dom (p ^ q) = (dom p) \/ (dom (Shift (q,(card p)))) by XBOOLE_0:def_3;
for x being set st x in (dom p) \/ (dom (Shift (q,(card p)))) holds
( ( x in dom (Shift (q,(card p))) implies (p ^ q) . x = (Shift (q,(card p))) . x ) & ( not x in dom (Shift (q,(card p))) implies (p ^ q) . x = p . x ) )
proof
let x be set ; ::_thesis: ( x in (dom p) \/ (dom (Shift (q,(card p)))) implies ( ( x in dom (Shift (q,(card p))) implies (p ^ q) . x = (Shift (q,(card p))) . x ) & ( not x in dom (Shift (q,(card p))) implies (p ^ q) . x = p . x ) ) )
assume A6: x in (dom p) \/ (dom (Shift (q,(card p)))) ; ::_thesis: ( ( x in dom (Shift (q,(card p))) implies (p ^ q) . x = (Shift (q,(card p))) . x ) & ( not x in dom (Shift (q,(card p))) implies (p ^ q) . x = p . x ) )
hereby ::_thesis: ( not x in dom (Shift (q,(card p))) implies (p ^ q) . x = p . x )
assume A7: x in dom (Shift (q,(card p))) ; ::_thesis: (p ^ q) . x = (Shift (q,(card p))) . x
then reconsider k = x as Nat ;
consider M being Element of NAT such that
A8: x = M + (card p) and
A9: M in dom q by A7, A1;
set m = k -' (len p);
A10: (len p) + (k -' (len p)) = k by A8, NAT_D:34;
hence (p ^ q) . x = q . (k -' (len p)) by A8, A9, Def3
.= (Shift (q,(card p))) . x by A8, A9, A10, VALUED_1:def_12 ;
::_thesis: verum
end;
assume not x in dom (Shift (q,(card p))) ; ::_thesis: (p ^ q) . x = p . x
then x in dom p by A6, XBOOLE_0:def_3;
hence (p ^ q) . x = p . x by Def3; ::_thesis: verum
end;
hence p ^ q = p +* (Shift (q,(card p))) by A5, FUNCT_4:def_1; ::_thesis: verum
end;
theorem :: AFINSQ_1:78
for p, q being XFinSequence holds
( p +* (p ^ q) = p ^ q & (p ^ q) +* p = p ^ q )
proof
let p, q be XFinSequence; ::_thesis: ( p +* (p ^ q) = p ^ q & (p ^ q) +* p = p ^ q )
p c= p ^ q by Th74;
hence ( p +* (p ^ q) = p ^ q & (p ^ q) +* p = p ^ q ) by FUNCT_4:97, FUNCT_4:98; ::_thesis: verum
end;
theorem Th79: :: AFINSQ_1:79
for n being Element of NAT
for I being NAT -defined finite initial Function
for J being Function holds dom (Shift (I,n)) misses dom (Shift (J,(n + (card I))))
proof
let n be Element of NAT ; ::_thesis: for I being NAT -defined finite initial Function
for J being Function holds dom (Shift (I,n)) misses dom (Shift (J,(n + (card I))))
let I be NAT -defined finite initial Function; ::_thesis: for J being Function holds dom (Shift (I,n)) misses dom (Shift (J,(n + (card I))))
let J be Function; ::_thesis: dom (Shift (I,n)) misses dom (Shift (J,(n + (card I))))
assume A1: dom (Shift (I,n)) meets dom (Shift (J,(n + (card I)))) ; ::_thesis: contradiction
dom (Shift (J,(n + (card I)))) = { (l + (n + (card I))) where l is Element of NAT : l in dom J } by VALUED_1:def_12;
then consider x being set such that
A2: x in dom (Shift (I,n)) and
A3: x in { (l + (n + (card I))) where l is Element of NAT : l in dom J } by A1, XBOOLE_0:3;
dom (Shift (I,n)) = { (m + n) where m is Element of NAT : m in dom I } by VALUED_1:def_12;
then consider m being Element of NAT such that
A4: x = m + n and
A5: m in dom I by A2;
consider l being Element of NAT such that
A6: x = l + (n + (card I)) and
l in dom J by A3;
m < card I by A5, NAT_1:44;
then l + (n + (card I)) < n + (card I) by A4, A6, XREAL_1:6;
hence contradiction by NAT_1:11; ::_thesis: verum
end;
theorem Th80: :: AFINSQ_1:80
for p, q being XFinSequence
for n being Element of NAT holds Shift (p,n) c= Shift ((p ^ q),n)
proof
let p, q be XFinSequence; ::_thesis: for n being Element of NAT holds Shift (p,n) c= Shift ((p ^ q),n)
let n be Element of NAT ; ::_thesis: Shift (p,n) c= Shift ((p ^ q),n)
p ^ q = p +* (Shift (q,(card p))) by Th77;
then A1: Shift ((p ^ q),n) = (Shift (p,n)) +* (Shift ((Shift (q,(card p))),n)) by VALUED_1:23;
Shift ((Shift (q,(card p))),n) = Shift (q,(n + (card p))) by VALUED_1:21;
then dom (Shift (p,n)) misses dom (Shift ((Shift (q,(card p))),n)) by Th79;
hence Shift (p,n) c= Shift ((p ^ q),n) by A1, FUNCT_4:32; ::_thesis: verum
end;
theorem Th81: :: AFINSQ_1:81
for q, p being XFinSequence
for n being Element of NAT holds Shift (q,(n + (card p))) c= Shift ((p ^ q),n)
proof
let q, p be XFinSequence; ::_thesis: for n being Element of NAT holds Shift (q,(n + (card p))) c= Shift ((p ^ q),n)
let n be Element of NAT ; ::_thesis: Shift (q,(n + (card p))) c= Shift ((p ^ q),n)
A1: Shift ((Shift (q,(card p))),n) = Shift (q,(n + (card p))) by VALUED_1:21;
p ^ q = p +* (Shift (q,(card p))) by Th77;
then Shift ((p ^ q),n) = (Shift (p,n)) +* (Shift ((Shift (q,(card p))),n)) by VALUED_1:23;
hence Shift (q,(n + (card p))) c= Shift ((p ^ q),n) by A1, FUNCT_4:25; ::_thesis: verum
end;
theorem :: AFINSQ_1:82
for X being set
for p, q being XFinSequence
for n being Element of NAT st Shift ((p ^ q),n) c= X holds
Shift (p,n) c= X
proof
let X be set ; ::_thesis: for p, q being XFinSequence
for n being Element of NAT st Shift ((p ^ q),n) c= X holds
Shift (p,n) c= X
let p, q be XFinSequence; ::_thesis: for n being Element of NAT st Shift ((p ^ q),n) c= X holds
Shift (p,n) c= X
let n be Element of NAT ; ::_thesis: ( Shift ((p ^ q),n) c= X implies Shift (p,n) c= X )
assume A1: Shift ((p ^ q),n) c= X ; ::_thesis: Shift (p,n) c= X
Shift (p,n) c= Shift ((p ^ q),n) by Th80;
hence Shift (p,n) c= X by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: AFINSQ_1:83
for X being set
for p, q being XFinSequence
for n being Element of NAT st Shift ((p ^ q),n) c= X holds
Shift (q,(n + (card p))) c= X
proof
let X be set ; ::_thesis: for p, q being XFinSequence
for n being Element of NAT st Shift ((p ^ q),n) c= X holds
Shift (q,(n + (card p))) c= X
let p, q be XFinSequence; ::_thesis: for n being Element of NAT st Shift ((p ^ q),n) c= X holds
Shift (q,(n + (card p))) c= X
let n be Element of NAT ; ::_thesis: ( Shift ((p ^ q),n) c= X implies Shift (q,(n + (card p))) c= X )
assume A1: Shift ((p ^ q),n) c= X ; ::_thesis: Shift (q,(n + (card p))) c= X
Shift (q,(n + (card p))) c= Shift ((p ^ q),n) by Th81;
hence Shift (q,(n + (card p))) c= X by A1, XBOOLE_1:1; ::_thesis: verum
end;
registration
let F be NAT -defined non empty finite initial Function;
cluster CutLastLoc F -> initial ;
coherence
CutLastLoc F is initial ;
end;
definition
let x1, x2, x3, x4 be set ;
func<%x1,x2,x3,x4%> -> set equals :: AFINSQ_1:def 14
((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>;
coherence
((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%> is set ;
end;
:: deftheorem defines <% AFINSQ_1:def_14_:_
for x1, x2, x3, x4 being set holds <%x1,x2,x3,x4%> = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>;
registration
let x1, x2, x3, x4 be set ;
cluster<%x1,x2,x3,x4%> -> Relation-like Function-like ;
coherence
( <%x1,x2,x3,x4%> is Function-like & <%x1,x2,x3,x4%> is Relation-like ) ;
end;
registration
let x1, x2, x3, x4 be set ;
cluster<%x1,x2,x3,x4%> -> T-Sequence-like finite ;
coherence
( <%x1,x2,x3,x4%> is finite & <%x1,x2,x3,x4%> is T-Sequence-like ) ;
end;
theorem :: AFINSQ_1:84
for x1, x2, x3, x4 being set holds len <%x1,x2,x3,x4%> = 4
proof
let x1, x2, x3, x4 be set ; ::_thesis: len <%x1,x2,x3,x4%> = 4
thus len <%x1,x2,x3,x4%> = (len <%x1,x2,x3%>) + 1 by Th75
.= 3 + 1 by Th39
.= 4 ; ::_thesis: verum
end;
theorem :: AFINSQ_1:85
for x1, x2, x3, x4 being set holds
( <%x1,x2,x3,x4%> . 0 = x1 & <%x1,x2,x3,x4%> . 1 = x2 & <%x1,x2,x3,x4%> . 2 = x3 & <%x1,x2,x3,x4%> . 3 = x4 )
proof
let x1, x2, x3, x4 be set ; ::_thesis: ( <%x1,x2,x3,x4%> . 0 = x1 & <%x1,x2,x3,x4%> . 1 = x2 & <%x1,x2,x3,x4%> . 2 = x3 & <%x1,x2,x3,x4%> . 3 = x4 )
thus <%x1,x2,x3,x4%> . 0 = ((<%x1%> ^ <%x2,x3%>) ^ <%x4%>) . 0 by Th27
.= (<%x1%> ^ <%x2,x3,x4%>) . 0 by Th27
.= x1 by Th35 ; ::_thesis: ( <%x1,x2,x3,x4%> . 1 = x2 & <%x1,x2,x3,x4%> . 2 = x3 & <%x1,x2,x3,x4%> . 3 = x4 )
A: len <%x1,x2,x3%> = 3 by Th39;
then B: 1 in dom <%x1,x2,x3%> by NAT_1:44;
thus <%x1,x2,x3,x4%> . 1 = <%x1,x2,x3%> . 1 by B, Def3
.= x2 by Th39 ; ::_thesis: ( <%x1,x2,x3,x4%> . 2 = x3 & <%x1,x2,x3,x4%> . 3 = x4 )
C: 2 in dom <%x1,x2,x3%> by A, NAT_1:44;
thus <%x1,x2,x3,x4%> . 2 = <%x1,x2,x3%> . 2 by C, Def3
.= x3 by Th39 ; ::_thesis: <%x1,x2,x3,x4%> . 3 = x4
thus <%x1,x2,x3,x4%> . 3 = x4 by A, Th36; ::_thesis: verum
end;