:: 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;