:: PRE_POLY semantic presentation begin definition let D be set ; let p, q be Element of D * ; :: original: ^ redefine funcp ^ q -> Element of D * ; coherence p ^ q is Element of D * proof p ^ q is FinSequence of D ; hence p ^ q is Element of D * by FINSEQ_1:def_11; ::_thesis: verum end; end; registration let D be set ; cluster Relation-like NAT -defined D -valued Function-like empty finite countable FinSequence-like FinSubsequence-like for Element of D * ; existence ex b1 being Element of D * st b1 is empty proof <*> D is Element of D * by FINSEQ_1:def_11; hence ex b1 being Element of D * st b1 is empty ; ::_thesis: verum end; end; definition let D be set ; :: original: <*> redefine func <*> D -> empty Element of D * ; coherence <*> D is empty Element of D * by FINSEQ_1:def_11; end; definition let D be non empty set ; let d be Element of D; :: original: <* redefine func<*d*> -> Element of D * ; coherence <*d*> is Element of D * proof <*d*> is FinSequence of D ; hence <*d*> is Element of D * by FINSEQ_1:def_11; ::_thesis: verum end; let e be Element of D; :: original: <* redefine func<*d,e*> -> Element of D * ; coherence <*d,e*> is Element of D * proof <*d,e*> = <*d*> ^ <*e*> by FINSEQ_1:def_9; hence <*d,e*> is Element of D * by FINSEQ_1:def_11; ::_thesis: verum end; end; begin registration let X be set ; cluster -> FinSequence-like for Element of X * ; coherence for b1 being Element of X * holds b1 is FinSequence-like ; end; definition let D be set ; let F be FinSequence of D * ; func FlattenSeq F -> Element of D * means :Def1: :: PRE_POLY:def 1 ex g being BinOp of (D *) st ( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & it = g "**" F ); existence ex b1 being Element of D * ex g being BinOp of (D *) st ( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b1 = g "**" F ) proof deffunc H1( Element of D * , Element of D * ) -> Element of D * = $1 ^ $2; consider g being BinOp of (D *) such that A1: for a, b being Element of D * holds g . (a,b) = H1(a,b) from BINOP_1:sch_4(); take g "**" F ; ::_thesis: ex g being BinOp of (D *) st ( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & g "**" F = g "**" F ) take g ; ::_thesis: ( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & g "**" F = g "**" F ) thus ( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & g "**" F = g "**" F ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Element of D * st ex g being BinOp of (D *) st ( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b1 = g "**" F ) & ex g being BinOp of (D *) st ( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b2 = g "**" F ) holds b1 = b2 proof let it1, it2 be Element of D * ; ::_thesis: ( ex g being BinOp of (D *) st ( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & it1 = g "**" F ) & ex g being BinOp of (D *) st ( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & it2 = g "**" F ) implies it1 = it2 ) given g1 being BinOp of (D *) such that A2: for p, q being Element of D * holds g1 . (p,q) = p ^ q and A3: it1 = g1 "**" F ; ::_thesis: ( for g being BinOp of (D *) holds ( ex p, q being Element of D * st not g . (p,q) = p ^ q or not it2 = g "**" F ) or it1 = it2 ) given g2 being BinOp of (D *) such that A4: for p, q being Element of D * holds g2 . (p,q) = p ^ q and A5: it2 = g2 "**" F ; ::_thesis: it1 = it2 now__::_thesis:_for_a,_b_being_Element_of_D_*_holds_g1_._(a,b)_=_g2_._(a,b) let a, b be Element of D * ; ::_thesis: g1 . (a,b) = g2 . (a,b) thus g1 . (a,b) = a ^ b by A2 .= g2 . (a,b) by A4 ; ::_thesis: verum end; hence it1 = it2 by A3, A5, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines FlattenSeq PRE_POLY:def_1_:_ for D being set for F being FinSequence of D * for b3 being Element of D * holds ( b3 = FlattenSeq F iff ex g being BinOp of (D *) st ( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b3 = g "**" F ) ); theorem Th1: :: PRE_POLY:1 for D being set for d being Element of D * holds FlattenSeq <*d*> = d proof let D be set ; ::_thesis: for d being Element of D * holds FlattenSeq <*d*> = d let d be Element of D * ; ::_thesis: FlattenSeq <*d*> = d ex g being BinOp of (D *) st ( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & FlattenSeq <*d*> = g "**" <*d*> ) by Def1; hence FlattenSeq <*d*> = d by FINSOP_1:11; ::_thesis: verum end; theorem Th2: :: PRE_POLY:2 for D being set holds FlattenSeq (<*> (D *)) = <*> D proof let D be set ; ::_thesis: FlattenSeq (<*> (D *)) = <*> D consider g being BinOp of (D *) such that A1: for d1, d2 being Element of D * holds g . (d1,d2) = d1 ^ d2 and A2: FlattenSeq (<*> (D *)) = g "**" (<*> (D *)) by Def1; A3: {} is Element of D * by FINSEQ_1:49; reconsider p = {} as Element of D * by FINSEQ_1:49; now__::_thesis:_for_a_being_Element_of_D_*_holds_ (_g_._({},a)_=_a_&_g_._(a,{})_=_a_) let a be Element of D * ; ::_thesis: ( g . ({},a) = a & g . (a,{}) = a ) thus g . ({},a) = {} ^ a by A1, A3 .= a by FINSEQ_1:34 ; ::_thesis: g . (a,{}) = a thus g . (a,{}) = a ^ {} by A1, A3 .= a by FINSEQ_1:34 ; ::_thesis: verum end; then A4: p is_a_unity_wrt g by BINOP_1:3; then g is having_a_unity by SETWISEO:def_2; then g "**" (<*> (D *)) = the_unity_wrt g by FINSOP_1:10; hence FlattenSeq (<*> (D *)) = <*> D by A2, A4, BINOP_1:def_8; ::_thesis: verum end; theorem Th3: :: PRE_POLY:3 for D being set for F, G being FinSequence of D * holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G) proof let D be set ; ::_thesis: for F, G being FinSequence of D * holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G) let F, G be FinSequence of D * ; ::_thesis: FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G) consider g being BinOp of (D *) such that A1: for d1, d2 being Element of D * holds g . (d1,d2) = d1 ^ d2 and A2: FlattenSeq (F ^ G) = g "**" (F ^ G) by Def1; now__::_thesis:_for_a,_b,_c_being_Element_of_D_*_holds_g_._(a,(g_._(b,c)))_=_g_._((g_._(a,b)),c) let a, b, c be Element of D * ; ::_thesis: g . (a,(g . (b,c))) = g . ((g . (a,b)),c) thus g . (a,(g . (b,c))) = a ^ (g . (b,c)) by A1 .= a ^ (b ^ c) by A1 .= (a ^ b) ^ c by FINSEQ_1:32 .= (g . (a,b)) ^ c by A1 .= g . ((g . (a,b)),c) by A1 ; ::_thesis: verum end; then A3: g is associative by BINOP_1:def_3; A4: {} is Element of D * by FINSEQ_1:49; reconsider p = {} as Element of D * by FINSEQ_1:49; now__::_thesis:_for_a_being_Element_of_D_*_holds_ (_g_._({},a)_=_a_&_g_._(a,{})_=_a_) let a be Element of D * ; ::_thesis: ( g . ({},a) = a & g . (a,{}) = a ) thus g . ({},a) = {} ^ a by A1, A4 .= a by FINSEQ_1:34 ; ::_thesis: g . (a,{}) = a thus g . (a,{}) = a ^ {} by A1, A4 .= a by FINSEQ_1:34 ; ::_thesis: verum end; then p is_a_unity_wrt g by BINOP_1:3; then ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) by SETWISEO:def_2; hence FlattenSeq (F ^ G) = g . ((g "**" F),(g "**" G)) by A2, A3, FINSOP_1:5 .= (g "**" F) ^ (g "**" G) by A1 .= (FlattenSeq F) ^ (g "**" G) by A1, Def1 .= (FlattenSeq F) ^ (FlattenSeq G) by A1, Def1 ; ::_thesis: verum end; theorem :: PRE_POLY:4 for D being set for p, q being Element of D * holds FlattenSeq <*p,q*> = p ^ q proof let D be set ; ::_thesis: for p, q being Element of D * holds FlattenSeq <*p,q*> = p ^ q let p, q be Element of D * ; ::_thesis: FlattenSeq <*p,q*> = p ^ q consider g being BinOp of (D *) such that A1: for d1, d2 being Element of D * holds g . (d1,d2) = d1 ^ d2 and A2: FlattenSeq <*p,q*> = g "**" <*p,q*> by Def1; thus FlattenSeq <*p,q*> = g . (p,q) by A2, FINSOP_1:12 .= p ^ q by A1 ; ::_thesis: verum end; theorem :: PRE_POLY:5 for D being set for p, q, r being Element of D * holds FlattenSeq <*p,q,r*> = (p ^ q) ^ r proof let D be set ; ::_thesis: for p, q, r being Element of D * holds FlattenSeq <*p,q,r*> = (p ^ q) ^ r let p, q, r be Element of D * ; ::_thesis: FlattenSeq <*p,q,r*> = (p ^ q) ^ r consider g being BinOp of (D *) such that A1: for d1, d2 being Element of D * holds g . (d1,d2) = d1 ^ d2 and A2: FlattenSeq <*p,q,r*> = g "**" <*p,q,r*> by Def1; thus FlattenSeq <*p,q,r*> = g . ((g . (p,q)),r) by A2, FINSOP_1:14 .= (g . (p,q)) ^ r by A1 .= (p ^ q) ^ r by A1 ; ::_thesis: verum end; theorem :: PRE_POLY:6 for D being set for F, G being FinSequence of D * st F c= G holds FlattenSeq F c= FlattenSeq G proof let D be set ; ::_thesis: for F, G being FinSequence of D * st F c= G holds FlattenSeq F c= FlattenSeq G let F, G be FinSequence of D * ; ::_thesis: ( F c= G implies FlattenSeq F c= FlattenSeq G ) assume F c= G ; ::_thesis: FlattenSeq F c= FlattenSeq G then consider F9 being FinSequence of D * such that A1: F ^ F9 = G by FINSEQ_4:82; (FlattenSeq F) ^ (FlattenSeq F9) = FlattenSeq G by A1, Th3; hence FlattenSeq F c= FlattenSeq G by FINSEQ_6:10; ::_thesis: verum end; begin scheme :: PRE_POLY:sch 1 Regr1{ F1() -> Nat, P1[ set ] } : for k being Element of NAT st k <= F1() holds P1[k] provided A1: P1[F1()] and A2: for k being Element of NAT st k < F1() & P1[k + 1] holds P1[k] proof reconsider n9 = F1() as Element of NAT by ORDINAL1:def_12; defpred S1[ Nat] means ( $1 <= F1() & P1[$1] ); assume ex k being Element of NAT st ( k <= F1() & P1[k] ) ; ::_thesis: contradiction then A3: ex k being Nat st S1[k] ; A4: for l being Nat st S1[l] holds l <= n9 ; consider l being Nat such that A5: S1[l] and A6: for n being Nat st S1[n] holds n <= l from NAT_1:sch_6(A4, A3); A7: l in NAT by ORDINAL1:def_12; A8: l < F1() by A1, A5, XXREAL_0:1; then l + 1 <= F1() by NAT_1:13; then P1[l + 1] by A6, XREAL_1:29; hence contradiction by A2, A5, A8, A7; ::_thesis: verum end; registration let n be Nat; cluster Seg (n + 1) -> non empty ; coherence not Seg (n + 1) is empty ; end; theorem :: PRE_POLY:7 for A being set holds {} |_2 A = {} ; registration let X be set ; cluster non empty for Element of bool (Fin X); existence not for b1 being Subset of (Fin X) holds b1 is empty proof {} in Fin X by FINSUB_1:7; then {{}} is Subset of (Fin X) by ZFMISC_1:31; hence not for b1 being Subset of (Fin X) holds b1 is empty ; ::_thesis: verum end; end; registration let X be non empty set ; cluster non empty with_non-empty_elements for Element of bool (Fin X); existence ex b1 being Subset of (Fin X) st ( not b1 is empty & b1 is with_non-empty_elements ) proof set x = the Element of X; { the Element of X} in Fin X by FINSUB_1:def_5; then reconsider s = {{ the Element of X}} as Subset of (Fin X) by SUBSET_1:33; take s ; ::_thesis: ( not s is empty & s is with_non-empty_elements ) thus not s is empty ; ::_thesis: s is with_non-empty_elements assume {} in s ; :: according to SETFAM_1:def_8 ::_thesis: contradiction hence contradiction ; ::_thesis: verum end; end; registration let X be non empty set ; let F be non empty with_non-empty_elements Subset of (Fin X); cluster non empty for Element of F; existence not for b1 being Element of F holds b1 is empty proof set f = the Element of F; the Element of F <> {} ; hence not for b1 being Element of F holds b1 is empty ; ::_thesis: verum end; end; registration let X be non empty set ; cluster with_non-empty_element for Element of bool (Fin X); existence ex b1 being Subset of (Fin X) st b1 is with_non-empty_element proof set x = the Element of X; { the Element of X} in Fin X by FINSUB_1:def_5; then reconsider s = {{ the Element of X}} as Subset of (Fin X) by SUBSET_1:33; take s ; ::_thesis: s is with_non-empty_element thus s is with_non-empty_element ; ::_thesis: verum end; end; definition let X be non empty set ; let R be Order of X; let A be Subset of X; :: original: |_2 redefine funcR |_2 A -> Order of A; coherence R |_2 A is Order of A proof R partially_orders X by ORDERS_1:44; hence R |_2 A is Order of A by ORDERS_1:35, ORDERS_1:45; ::_thesis: verum end; end; scheme :: PRE_POLY:sch 2 SubFinite{ F1() -> set , F2() -> Subset of F1(), P1[ set ] } : P1[F2()] provided A1: F2() is finite and A2: P1[ {} F1()] and A3: for x being Element of F1() for B being Subset of F1() st x in F2() & B c= F2() & P1[B] holds P1[B \/ {x}] proof now__::_thesis:_(_F2()_<>_{}_implies_P1[F2()]_) defpred S1[ set ] means ex B being set st ( B = $1 & P1[B] ); assume F2() <> {} ; ::_thesis: P1[F2()] consider G being set such that A4: for x being set holds ( x in G iff ( x in bool F2() & S1[x] ) ) from XBOOLE_0:sch_1(); G c= bool F2() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in G or x in bool F2() ) assume x in G ; ::_thesis: x in bool F2() hence x in bool F2() by A4; ::_thesis: verum end; then reconsider GA = G as Subset-Family of F2() ; {} c= F2() by XBOOLE_1:2; then GA <> {} by A2, A4; then consider B being set such that A5: B in GA and A6: for X being set st X in GA & B c= X holds B = X by A1, FINSET_1:6; A7: ex A being set st ( A = B & P1[A] ) by A4, A5; now__::_thesis:_not_B_<>_F2() set x = the Element of F2() \ B; assume B <> F2() ; ::_thesis: contradiction then not F2() c= B by A5, XBOOLE_0:def_10; then A8: F2() \ B <> {} by XBOOLE_1:37; then not the Element of F2() \ B in B by XBOOLE_0:def_5; then not { the Element of F2() \ B} c= B by ZFMISC_1:31; then A9: B \/ { the Element of F2() \ B} <> B by XBOOLE_1:7; A10: the Element of F2() \ B in F2() by A8, XBOOLE_0:def_5; then { the Element of F2() \ B} c= F2() by ZFMISC_1:31; then A11: B \/ { the Element of F2() \ B} c= F2() by A5, XBOOLE_1:8; B is Subset of F1() by A5, XBOOLE_1:1; then P1[B \/ { the Element of F2() \ B}] by A3, A5, A7, A10; then B \/ { the Element of F2() \ B} in GA by A4, A11; hence contradiction by A6, A9, XBOOLE_1:7; ::_thesis: verum end; hence P1[F2()] by A7; ::_thesis: verum end; hence P1[F2()] by A2; ::_thesis: verum end; registration let X be non empty set ; let F be with_non-empty_element Subset of (Fin X); cluster non empty finite for Element of F; existence ex b1 being Element of F st ( b1 is finite & not b1 is empty ) proof consider x being non empty set such that A1: x in F by SETFAM_1:def_10; reconsider x1 = x as Element of F by A1; take x1 ; ::_thesis: ( x1 is finite & not x1 is empty ) thus ( x1 is finite & not x1 is empty ) ; ::_thesis: verum end; end; theorem Th8: :: PRE_POLY:8 for A, B being finite set st A c= B & card A = card B holds A = B proof let A, B be finite set ; ::_thesis: ( A c= B & card A = card B implies A = B ) assume A1: A c= B ; ::_thesis: ( not card A = card B or A = B ) assume A2: card A = card B ; ::_thesis: A = B reconsider A = A as Subset of B by A1; set f = incl A; rng (incl A) = B by A2, FINSEQ_4:63; hence A = B ; ::_thesis: verum end; definition let X be set ; let A be finite Subset of X; let R be Order of X; assume A1: R linearly_orders A ; func SgmX (R,A) -> FinSequence of X means :Def2: :: PRE_POLY:def 2 ( rng it = A & ( for n, m being Nat st n in dom it & m in dom it & n < m holds ( it /. n <> it /. m & [(it /. n),(it /. m)] in R ) ) ); existence ex b1 being FinSequence of X st ( rng b1 = A & ( for n, m being Nat st n in dom b1 & m in dom b1 & n < m holds ( b1 /. n <> b1 /. m & [(b1 /. n),(b1 /. m)] in R ) ) ) proof percases ( A is empty or not A is empty ) ; supposeA2: A is empty ; ::_thesis: ex b1 being FinSequence of X st ( rng b1 = A & ( for n, m being Nat st n in dom b1 & m in dom b1 & n < m holds ( b1 /. n <> b1 /. m & [(b1 /. n),(b1 /. m)] in R ) ) ) take <*> X ; ::_thesis: ( rng (<*> X) = A & ( for n, m being Nat st n in dom (<*> X) & m in dom (<*> X) & n < m holds ( (<*> X) /. n <> (<*> X) /. m & [((<*> X) /. n),((<*> X) /. m)] in R ) ) ) thus ( rng (<*> X) = A & ( for n, m being Nat st n in dom (<*> X) & m in dom (<*> X) & n < m holds ( (<*> X) /. n <> (<*> X) /. m & [((<*> X) /. n),((<*> X) /. m)] in R ) ) ) by A2; ::_thesis: verum end; supposeA3: not A is empty ; ::_thesis: ex b1 being FinSequence of X st ( rng b1 = A & ( for n, m being Nat st n in dom b1 & m in dom b1 & n < m holds ( b1 /. n <> b1 /. m & [(b1 /. n),(b1 /. m)] in R ) ) ) then reconsider X9 = X as non empty set ; reconsider A1 = A as non empty finite Subset of X9 by A3; reconsider R9 = R as Order of X9 ; deffunc H1( set ) -> set = $1; deffunc H2( Element of A1) -> set = { H1(x) where x is Element of A1 : ( x <=_ R9,$1 & x <> $1 ) } ; deffunc H3( Element of A1) -> set = (card H2($1)) +^ 1; A4: for x being Element of A1 holds H3(x) is Element of NAT proof let a be Element of A1; ::_thesis: H3(a) is Element of NAT defpred S1[ Element of A1] means ( $1 <=_ R9,a & $1 <> a ); { H1(x) where x is Element of A1 : S1[x] } is finite from PRE_CIRC:sch_1(); then reconsider X = { H1(x) where x is Element of A1 : S1[x] } as finite set ; reconsider n = card X as Element of NAT ; n +^ 1 = n + 1 by CARD_2:36; hence H3(a) is Element of NAT ; ::_thesis: verum end; consider f being Function of A1,NAT such that A5: for x being Element of A1 holds f . x = H3(x) from FUNCT_2:sch_9(A4); A6: for x being Element of A1 holds not x in H2(x) proof let a be Element of A1; ::_thesis: not a in H2(a) assume a in H2(a) ; ::_thesis: contradiction then ex x being Element of A1 st ( x = a & x <=_ R9,a & x <> a ) ; hence contradiction ; ::_thesis: verum end; A7: for x being Element of A1 holds H2(x) c= A1 proof let a be Element of A1; ::_thesis: H2(a) c= A1 let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in H2(a) or y in A1 ) assume y in H2(a) ; ::_thesis: y in A1 then ex x being Element of A1 st ( x = y & x <=_ R9,a & x <> a ) ; hence y in A1 ; ::_thesis: verum end; rng f c= Seg (card A1) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Seg (card A1) ) assume y in rng f ; ::_thesis: y in Seg (card A1) then consider x1 being set such that A8: x1 in dom f and A9: y = f . x1 by FUNCT_1:def_3; reconsider y1 = y as Nat by A9; reconsider x2 = x1 as Element of A1 by A8; defpred S1[ Element of A1] means ( $1 <=_ R9,x2 & $1 <> x2 ); { H1(x) where x is Element of A1 : S1[x] } is finite from PRE_CIRC:sch_1(); then reconsider Vx2 = H2(x2) as finite set ; Vx2 <> A1 by A6; then A10: card Vx2 <> card A1 by A7, Th8; card Vx2 <= card A1 by A7, NAT_1:43; then card Vx2 < card A1 by A10, XXREAL_0:1; then A11: (card Vx2) + 1 <= card A1 by NAT_1:13; A12: y = (card Vx2) +^ 1 by A5, A9 .= (card Vx2) + 1 by CARD_2:36 ; then 0 + 1 <= y1 by XREAL_1:6; hence y in Seg (card A1) by A11, A12, FINSEQ_1:1; ::_thesis: verum end; then reconsider f1 = f as Function of A1,(Seg (card A1)) by FUNCT_2:6; A13: R |_2 A c= R by XBOOLE_1:17; A14: R is_connected_in A by A1, ORDERS_1:def_8; then A15: R |_2 A is connected by ORDERS_1:75; field (R9 |_2 A1) = A by ORDERS_1:15; then A16: R |_2 A is_connected_in A by A15, RELAT_2:def_14; A17: R9 is_transitive_in A by A1, ORDERS_1:def_8; A18: R9 is_antisymmetric_in A by A1, ORDERS_1:def_8; for x1, x2 being set st x1 in A1 & x2 in A1 & f . x1 = f . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in A1 & x2 in A1 & f . x1 = f . x2 implies x1 = x2 ) assume that A19: x1 in A1 and A20: x2 in A1 and A21: f . x1 = f . x2 ; ::_thesis: x1 = x2 reconsider x29 = x2 as Element of A1 by A20; reconsider x19 = x1 as Element of A1 by A19; defpred S1[ Element of A1] means ( $1 <=_ R9,x19 & $1 <> x19 ); { H1(x) where x is Element of A1 : S1[x] } is finite from PRE_CIRC:sch_1(); then reconsider Vx1 = H2(x19) as finite set ; defpred S2[ Element of A1] means ( $1 <=_ R9,x29 & $1 <> x29 ); { H1(x) where x is Element of A1 : S2[x] } is finite from PRE_CIRC:sch_1(); then reconsider Vx2 = H2(x29) as finite set ; A22: for x1, x2 being Element of A1 st x1 <=_ R |_2 A,x2 holds H2(x1) c= H2(x2) proof let x1, x2 be Element of A1; ::_thesis: ( x1 <=_ R |_2 A,x2 implies H2(x1) c= H2(x2) ) assume x1 <=_ R |_2 A,x2 ; ::_thesis: H2(x1) c= H2(x2) then A23: [x1,x2] in R |_2 A by ARROW:def_4; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H2(x1) or x in H2(x2) ) assume x in H2(x1) ; ::_thesis: x in H2(x2) then consider a being Element of A such that A24: a = x and A25: a <=_ R9,x1 and A26: a <> x1 ; A27: [a,x1] in R9 by A25, ARROW:def_4; then [a,x2] in R9 by A23, A13, A17, RELAT_2:def_8; then A28: a <=_ R9,x2 by ARROW:def_4; a <> x2 by A26, A27, A23, A13, A18, RELAT_2:def_4; hence x in H2(x2) by A24, A28; ::_thesis: verum end; f . x19 = (card Vx1) +^ 1 by A5 .= (card Vx1) + 1 by CARD_2:36 ; then A29: (card Vx1) + 1 = (card Vx2) +^ 1 by A5, A21 .= (card Vx2) + 1 by CARD_2:36 ; now__::_thesis:_x1_=_x2 percases ( x19 = x29 or x19 <> x29 ) ; suppose x19 = x29 ; ::_thesis: x1 = x2 hence x1 = x2 ; ::_thesis: verum end; suppose x19 <> x29 ; ::_thesis: x1 = x2 then A30: ( [x19,x29] in R |_2 A or [x29,x19] in R |_2 A ) by A16, RELAT_2:def_6; A31: for x1, x2 being Element of A1 st x1 <> x2 & x1 <=_ R |_2 A,x2 holds x1 in H2(x2) proof let x1, x2 be Element of A1; ::_thesis: ( x1 <> x2 & x1 <=_ R |_2 A,x2 implies x1 in H2(x2) ) assume A32: x1 <> x2 ; ::_thesis: ( not x1 <=_ R |_2 A,x2 or x1 in H2(x2) ) assume x1 <=_ R |_2 A,x2 ; ::_thesis: x1 in H2(x2) then [x1,x2] in R |_2 A by ARROW:def_4; then x1 <=_ R9,x2 by A13, ARROW:def_4; hence x1 in H2(x2) by A32; ::_thesis: verum end; A33: now__::_thesis:_Vx1_=_Vx2 percases ( x19 <=_ R |_2 A,x29 or x29 <=_ R |_2 A,x19 ) by A30, ARROW:def_4; suppose x19 <=_ R |_2 A,x29 ; ::_thesis: Vx1 = Vx2 hence Vx1 = Vx2 by A29, Th8, A22; ::_thesis: verum end; suppose x29 <=_ R |_2 A,x19 ; ::_thesis: Vx1 = Vx2 hence Vx1 = Vx2 by A29, Th8, A22; ::_thesis: verum end; end; end; now__::_thesis:_not_x19_<>_x29 assume A34: x19 <> x29 ; ::_thesis: contradiction then A35: ( [x19,x29] in R |_2 A or [x29,x19] in R |_2 A ) by A16, RELAT_2:def_6; percases ( x19 <=_ R |_2 A,x29 or x29 <=_ R |_2 A,x19 ) by A35, ARROW:def_4; suppose x19 <=_ R |_2 A,x29 ; ::_thesis: contradiction hence contradiction by A33, A6, A34, A31; ::_thesis: verum end; suppose x29 <=_ R |_2 A,x19 ; ::_thesis: contradiction hence contradiction by A33, A6, A34, A31; ::_thesis: verum end; end; end; hence x1 = x2 ; ::_thesis: verum end; end; end; hence x1 = x2 ; ::_thesis: verum end; then A36: f1 is one-to-one by FUNCT_2:19; A37: for x1, x2 being Element of A1 st f . x1 < f . x2 holds ( x1 <=_ R9,x2 & x1 <> x2 ) proof let x1, x2 be Element of A1; ::_thesis: ( f . x1 < f . x2 implies ( x1 <=_ R9,x2 & x1 <> x2 ) ) defpred S1[ Element of A1] means ( $1 <=_ R9,x1 & $1 <> x1 ); { H1(x) where x is Element of A1 : S1[x] } is finite from PRE_CIRC:sch_1(); then reconsider Vx1 = H2(x1) as finite set ; defpred S2[ Element of A1] means ( $1 <=_ R9,x2 & $1 <> x2 ); { H1(x) where x is Element of A1 : S2[x] } is finite from PRE_CIRC:sch_1(); then reconsider Vx2 = H2(x2) as finite set ; assume A38: f . x1 < f . x2 ; ::_thesis: ( x1 <=_ R9,x2 & x1 <> x2 ) A39: f . x1 = (card Vx1) +^ 1 by A5 .= (card Vx1) + 1 by CARD_2:36 ; f . x2 = (card Vx2) +^ 1 by A5 .= (card Vx2) + 1 by CARD_2:36 ; then A40: ((card Vx1) + 1) - 1 < ((card Vx2) + 1) - 1 by A39, A38, XREAL_1:9; reconsider Cx2 = card Vx2 as Cardinal ; reconsider Cx1 = card Vx1 as Cardinal ; A41: card (card Vx2) = card Vx2 ; card (card Vx1) = card Vx1 ; then Cx1 in Cx2 by A41, A40, NAT_1:41; then Vx2 \ Vx1 <> {} by CARD_1:68; then consider a being set such that A42: a in Vx2 \ Vx1 by XBOOLE_0:def_1; A43: not a in Vx1 by A42, XBOOLE_0:def_5; A44: a in Vx2 by A42; Vx2 c= A1 by A7; then reconsider a = a as Element of A1 by A44; A45: ex x being Element of A1 st ( a = x & x <=_ R9,x2 & x <> x2 ) by A44; then A46: [a,x2] in R9 by ARROW:def_4; now__::_thesis:_(_x1_<=__R9,x2_&_x1_<>_x2_) percases ( not a <=_ R9,x1 or a = x1 ) by A43; suppose not a <=_ R9,x1 ; ::_thesis: ( x1 <=_ R9,x2 & x1 <> x2 ) then A47: not [a,x1] in R9 by ARROW:def_4; now__::_thesis:_(_x1_<=__R9,x2_&_x1_<>_x2_) percases ( x1 = a or x1 <> a ) ; suppose x1 = a ; ::_thesis: ( x1 <=_ R9,x2 & x1 <> x2 ) hence ( x1 <=_ R9,x2 & x1 <> x2 ) by A45; ::_thesis: verum end; supposeA48: x1 <> a ; ::_thesis: ( x1 <=_ R9,x2 & not x1 = x2 ) then A49: [x1,a] in R9 by A14, A47, RELAT_2:def_6; then [x1,x2] in R9 by A46, A17, RELAT_2:def_8; hence x1 <=_ R9,x2 by ARROW:def_4; ::_thesis: not x1 = x2 assume x1 = x2 ; ::_thesis: contradiction then a = x1 by A49, A46, A18, RELAT_2:def_4; hence contradiction by A48; ::_thesis: verum end; end; end; hence ( x1 <=_ R9,x2 & x1 <> x2 ) ; ::_thesis: verum end; suppose a = x1 ; ::_thesis: ( x1 <=_ R9,x2 & x1 <> x2 ) hence ( x1 <=_ R9,x2 & x1 <> x2 ) by A45; ::_thesis: verum end; end; end; hence ( x1 <=_ R9,x2 & x1 <> x2 ) ; ::_thesis: verum end; card (Seg (card A1)) = card A1 by FINSEQ_1:57; then rng f1 = Seg (card A1) by A36, FINSEQ_4:63; then dom (f1 ") = Seg (card A1) by A36, FUNCT_1:33; then reconsider g1 = f1 " as FinSequence by FINSEQ_1:def_2; A50: dom f1 = A by FUNCT_2:def_1; then A51: rng g1 = A by A36, FUNCT_1:33; then reconsider g = g1 as FinSequence of X by FINSEQ_1:def_4; take g ; ::_thesis: ( rng g = A & ( for n, m being Nat st n in dom g & m in dom g & n < m holds ( g /. n <> g /. m & [(g /. n),(g /. m)] in R ) ) ) thus rng g = A by A36, A50, FUNCT_1:33; ::_thesis: for n, m being Nat st n in dom g & m in dom g & n < m holds ( g /. n <> g /. m & [(g /. n),(g /. m)] in R ) let n, m be Nat; ::_thesis: ( n in dom g & m in dom g & n < m implies ( g /. n <> g /. m & [(g /. n),(g /. m)] in R ) ) assume that A52: n in dom g and A53: m in dom g and A54: n < m ; ::_thesis: ( g /. n <> g /. m & [(g /. n),(g /. m)] in R ) reconsider gn = g . n as Element of A1 by A51, A52, FUNCT_1:def_3; n in rng f by A36, A52, FUNCT_1:33; then A55: n = f . gn by A36, FUNCT_1:35; reconsider gm = g . m as Element of A1 by A51, A53, FUNCT_1:def_3; A56: gm = g /. m by A53, PARTFUN1:def_6; A57: m in rng f by A36, A53, FUNCT_1:33; then m = f . gm by A36, FUNCT_1:35; then gn <=_ R9,gm by A37, A54, A55; then [gn,gm] in R by ARROW:def_4; then A58: [gn,gm] in R |_2 A by XBOOLE_0:def_4; gn = g /. n by A52, PARTFUN1:def_6; hence ( g /. n <> g /. m & [(g /. n),(g /. m)] in R ) by A36, A54, A57, A55, A13, A58, A56, FUNCT_1:35; ::_thesis: verum end; end; end; uniqueness for b1, b2 being FinSequence of X st rng b1 = A & ( for n, m being Nat st n in dom b1 & m in dom b1 & n < m holds ( b1 /. n <> b1 /. m & [(b1 /. n),(b1 /. m)] in R ) ) & rng b2 = A & ( for n, m being Nat st n in dom b2 & m in dom b2 & n < m holds ( b2 /. n <> b2 /. m & [(b2 /. n),(b2 /. m)] in R ) ) holds b1 = b2 proof let p9, q9 be FinSequence of X; ::_thesis: ( rng p9 = A & ( for n, m being Nat st n in dom p9 & m in dom p9 & n < m holds ( p9 /. n <> p9 /. m & [(p9 /. n),(p9 /. m)] in R ) ) & rng q9 = A & ( for n, m being Nat st n in dom q9 & m in dom q9 & n < m holds ( q9 /. n <> q9 /. m & [(q9 /. n),(q9 /. m)] in R ) ) implies p9 = q9 ) assume that A59: rng p9 = A and A60: for n, m being Nat st n in dom p9 & m in dom p9 & n < m holds ( p9 /. n <> p9 /. m & [(p9 /. n),(p9 /. m)] in R ) and A61: rng q9 = A and A62: for n, m being Nat st n in dom q9 & m in dom q9 & n < m holds ( q9 /. n <> q9 /. m & [(q9 /. n),(q9 /. m)] in R ) ; ::_thesis: p9 = q9 percases ( A is empty or not A is empty ) ; supposeA63: A is empty ; ::_thesis: p9 = q9 then p9 is empty by A59; hence p9 = q9 by A61, A63; ::_thesis: verum end; supposeA64: not A is empty ; ::_thesis: p9 = q9 then reconsider X9 = X as non empty set ; reconsider A9 = A as non empty finite Subset of X9 by A64; set E = <*> A9; defpred S1[ FinSequence of A9] means ( $1 is FinSequence of A9 & ( for n, m being Nat st n in dom $1 & m in dom $1 & n < m holds ( $1 /. n <> $1 /. m & [($1 /. n),($1 /. m)] in R ) ) implies for q being FinSequence of A9 st rng q = rng $1 & ( for n, m being Nat st n in dom q & m in dom q & n < m holds ( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) ) holds q = $1 ); reconsider p = p9, q = q9 as FinSequence of A9 by A59, A61, FINSEQ_1:def_4; A65: for p being FinSequence of A9 for x being Element of A9 st S1[p] holds S1[p ^ <*x*>] proof let p be FinSequence of A9; ::_thesis: for x being Element of A9 st S1[p] holds S1[p ^ <*x*>] let x be Element of A9; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] ) assume A66: S1[p] ; ::_thesis: S1[p ^ <*x*>] assume p ^ <*x*> is FinSequence of A9 ; ::_thesis: ( ex n, m being Nat st ( n in dom (p ^ <*x*>) & m in dom (p ^ <*x*>) & n < m & not ( (p ^ <*x*>) /. n <> (p ^ <*x*>) /. m & [((p ^ <*x*>) /. n),((p ^ <*x*>) /. m)] in R ) ) or for q being FinSequence of A9 st rng q = rng (p ^ <*x*>) & ( for n, m being Nat st n in dom q & m in dom q & n < m holds ( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) ) holds q = p ^ <*x*> ) assume A67: for n, m being Nat st n in dom (p ^ <*x*>) & m in dom (p ^ <*x*>) & n < m holds ( (p ^ <*x*>) /. n <> (p ^ <*x*>) /. m & [((p ^ <*x*>) /. n),((p ^ <*x*>) /. m)] in R ) ; ::_thesis: for q being FinSequence of A9 st rng q = rng (p ^ <*x*>) & ( for n, m being Nat st n in dom q & m in dom q & n < m holds ( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) ) holds q = p ^ <*x*> let q be FinSequence of A9; ::_thesis: ( rng q = rng (p ^ <*x*>) & ( for n, m being Nat st n in dom q & m in dom q & n < m holds ( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) ) implies q = p ^ <*x*> ) assume that A68: rng q = rng (p ^ <*x*>) and A69: for n, m being Nat st n in dom q & m in dom q & n < m holds ( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) ; ::_thesis: q = p ^ <*x*> deffunc H1( Nat) -> set = q . $1; A70: q <> 0 by A68; then consider n being Nat such that A71: len q = n + 1 by NAT_1:6; reconsider n = n as Element of NAT by ORDINAL1:def_12; ex q9 being FinSequence st ( len q9 = n & ( for m being Nat st m in dom q9 holds q9 . m = H1(m) ) ) from FINSEQ_1:sch_2(); then consider q9 being FinSequence such that A72: len q9 = n and A73: for m being Nat st m in dom q9 holds q9 . m = q . m ; 1 in Seg 1 by FINSEQ_1:2, TARSKI:def_1; then A74: 1 in dom <*x*> by FINSEQ_1:def_8; A75: ex m being Element of A9 st ( m = x & ( for l being Element of A9 st l in rng (p ^ <*x*>) & l <> x holds [l,m] in R ) ) proof reconsider m = x as Element of A9 ; take m ; ::_thesis: ( m = x & ( for l being Element of A9 st l in rng (p ^ <*x*>) & l <> x holds [l,m] in R ) ) thus m = x ; ::_thesis: for l being Element of A9 st l in rng (p ^ <*x*>) & l <> x holds [l,m] in R thus for l being Element of A9 st l in rng (p ^ <*x*>) & l <> x holds [l,m] in R ::_thesis: verum proof let l be Element of A9; ::_thesis: ( l in rng (p ^ <*x*>) & l <> x implies [l,m] in R ) assume that A76: l in rng (p ^ <*x*>) and A77: l <> x ; ::_thesis: [l,m] in R consider y being set such that A78: y in dom (p ^ <*x*>) and A79: l = (p ^ <*x*>) . y by A76, FUNCT_1:def_3; A80: l = (p ^ <*x*>) /. y by A78, A79, PARTFUN1:def_6; reconsider k = y as Element of NAT by A78; A81: k <> (len p) + 1 proof assume k = (len p) + 1 ; ::_thesis: contradiction then (p ^ <*x*>) . k = <*x*> . 1 by A74, FINSEQ_1:def_7 .= x by FINSEQ_1:def_8 ; hence contradiction by A77, A79; ::_thesis: verum end; A82: y in Seg (len (p ^ <*x*>)) by A78, FINSEQ_1:def_3; then k <= len (p ^ <*x*>) by FINSEQ_1:1; then k <= (len p) + (len <*x*>) by FINSEQ_1:22; then k <= (len p) + 1 by FINSEQ_1:39; then k < (len p) + 1 by A81, XXREAL_0:1; then k < (len p) + (len <*x*>) by FINSEQ_1:39; then A83: k < len (p ^ <*x*>) by FINSEQ_1:22; 1 <= k by A82, FINSEQ_1:1; then 1 - (len (p ^ <*x*>)) < k - k by A83, XREAL_1:15; then 1 < len (p ^ <*x*>) by XREAL_1:48; then len (p ^ <*x*>) in Seg (len (p ^ <*x*>)) by FINSEQ_1:1; then A84: len (p ^ <*x*>) in dom (p ^ <*x*>) by FINSEQ_1:def_3; m = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42 .= (p ^ <*x*>) . ((len p) + (len <*x*>)) by FINSEQ_1:39 .= (p ^ <*x*>) . (len (p ^ <*x*>)) by FINSEQ_1:22 ; then m = (p ^ <*x*>) /. (len (p ^ <*x*>)) by A84, PARTFUN1:def_6; hence [l,m] in R by A67, A78, A80, A83, A84; ::_thesis: verum end; end; A85: for m being Nat st m in dom <*x*> holds q . ((len q9) + m) = <*x*> . m proof let m be Nat; ::_thesis: ( m in dom <*x*> implies q . ((len q9) + m) = <*x*> . m ) assume m in dom <*x*> ; ::_thesis: q . ((len q9) + m) = <*x*> . m then A86: m in {1} by FINSEQ_1:2, FINSEQ_1:def_8; A87: q . ((len q9) + m) = x proof consider d1 being Element of A9 such that A88: d1 = x and A89: for l being Element of A9 st l in rng (p ^ <*x*>) & l <> x holds [l,d1] in R by A75; reconsider d = d1 as Element of A9 ; len q in Seg (len q) by A70, FINSEQ_1:3; then A90: len q in dom q by FINSEQ_1:def_3; then q . (len q) in rng q by FUNCT_1:def_3; then reconsider k = q . (len q) as Element of A9 ; A91: k = q /. (len q) by A90, PARTFUN1:def_6; field R = X by ORDERS_1:12; then A92: R is_antisymmetric_in X by RELAT_2:def_12; assume q . ((len q9) + m) <> x ; ::_thesis: contradiction then A93: q . (len q) <> x by A71, A72, A86, TARSKI:def_1; x in {x} by TARSKI:def_1; then x in rng <*x*> by FINSEQ_1:38; then x in (rng p) \/ (rng <*x*>) by XBOOLE_0:def_3; then x in rng q by A68, FINSEQ_1:31; then consider y being set such that A94: y in dom q and A95: x = q . y by FUNCT_1:def_3; A96: y in Seg (len q) by A94, FINSEQ_1:def_3; reconsider y = y as Element of NAT by A94; y <= len q by A96, FINSEQ_1:1; then A97: y < len q by A93, A95, XXREAL_0:1; q . (len q) in rng (p ^ <*x*>) by A68, A90, FUNCT_1:def_3; then A98: [k,d] in R by A93, A89; A99: d = q /. y by A88, A94, A95, PARTFUN1:def_6; then A100: [d,k] in R by A69, A94, A90, A97, A91; k <> d by A69, A94, A90, A97, A91, A99; hence contradiction by A98, A100, A92, RELAT_2:def_4; ::_thesis: verum end; m = 1 by A86, TARSKI:def_1; hence q . ((len q9) + m) = <*x*> . m by A87, FINSEQ_1:40; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_rng_q9_holds_ x_in_A9 let x be set ; ::_thesis: ( x in rng q9 implies x in A9 ) A101: n <= n + 1 by NAT_1:11; assume x in rng q9 ; ::_thesis: x in A9 then consider y being set such that A102: y in dom q9 and A103: x = q9 . y by FUNCT_1:def_3; A104: y in Seg (len q9) by A102, FINSEQ_1:def_3; reconsider y = y as Element of NAT by A102; y <= n by A72, A104, FINSEQ_1:1; then A105: y <= n + 1 by A101, XXREAL_0:2; 1 <= y by A104, FINSEQ_1:1; then y in dom q by A71, A105, FINSEQ_3:25; then q . y in rng q by FUNCT_1:def_3; then q . y in A9 ; hence x in A9 by A73, A102, A103; ::_thesis: verum end; then rng q9 c= A9 by TARSKI:def_3; then reconsider f = q9 as FinSequence of A9 by FINSEQ_1:def_4; dom q = Seg (n + 1) by A71, FINSEQ_1:def_3 .= Seg ((len q9) + (len <*x*>)) by A72, FINSEQ_1:39 ; then A106: q9 ^ <*x*> = q by A73, A85, FINSEQ_1:def_7; A107: not x in rng p proof (len p) + 1 = (len p) + (len <*x*>) by FINSEQ_1:39 .= len (p ^ <*x*>) by FINSEQ_1:22 ; then (len p) + 1 in Seg (len (p ^ <*x*>)) by FINSEQ_1:4; then A108: (len p) + 1 in dom (p ^ <*x*>) by FINSEQ_1:def_3; assume x in rng p ; ::_thesis: contradiction then consider y being set such that A109: y in dom p and A110: x = p . y by FUNCT_1:def_3; A111: y in Seg (len p) by A109, FINSEQ_1:def_3; A112: dom p c= dom (p ^ <*x*>) by FINSEQ_1:26; reconsider y = y as Element of NAT by A109; x = (p ^ <*x*>) . y by A109, A110, FINSEQ_1:def_7; then A113: x = (p ^ <*x*>) /. y by A109, A112, PARTFUN1:def_6; y <= len p by A111, FINSEQ_1:1; then A114: y < (len p) + 1 by NAT_1:13; x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42; then (p ^ <*x*>) /. y = (p ^ <*x*>) /. ((len p) + 1) by A108, A113, PARTFUN1:def_6; hence contradiction by A67, A109, A108, A112, A114; ::_thesis: verum end; A115: for z being set holds ( z in ((rng p) \/ {x}) \ {x} iff z in rng p ) proof let z be set ; ::_thesis: ( z in ((rng p) \/ {x}) \ {x} iff z in rng p ) thus ( z in ((rng p) \/ {x}) \ {x} implies z in rng p ) ::_thesis: ( z in rng p implies z in ((rng p) \/ {x}) \ {x} ) proof assume A116: z in ((rng p) \/ {x}) \ {x} ; ::_thesis: z in rng p then A117: not z in {x} by XBOOLE_0:def_5; z in (rng p) \/ {x} by A116, XBOOLE_0:def_5; hence z in rng p by A117, XBOOLE_0:def_3; ::_thesis: verum end; assume A118: z in rng p ; ::_thesis: z in ((rng p) \/ {x}) \ {x} then A119: z in (rng p) \/ {x} by XBOOLE_0:def_3; not z in {x} by A107, A118, TARSKI:def_1; hence z in ((rng p) \/ {x}) \ {x} by A119, XBOOLE_0:def_5; ::_thesis: verum end; rng (p ^ <*x*>) = (rng p) \/ (rng <*x*>) by FINSEQ_1:31 .= (rng p) \/ {x} by FINSEQ_1:39 ; then A120: rng p = (rng (p ^ <*x*>)) \ {x} by A115, TARSKI:1; A121: ( rng f = rng p & ( for l, m being Nat st l in dom f & m in dom f & l < m holds ( f /. l <> f /. m & [(f /. l),(f /. m)] in R ) ) ) proof A122: not x in rng f proof (len f) + 1 = (len f) + (len <*x*>) by FINSEQ_1:39 .= len (f ^ <*x*>) by FINSEQ_1:22 ; then (len f) + 1 in Seg (len (f ^ <*x*>)) by FINSEQ_1:4; then A123: (len f) + 1 in dom (f ^ <*x*>) by FINSEQ_1:def_3; assume x in rng f ; ::_thesis: contradiction then consider y being set such that A124: y in dom f and A125: x = f . y by FUNCT_1:def_3; A126: y in Seg (len f) by A124, FINSEQ_1:def_3; A127: dom f c= dom (f ^ <*x*>) by FINSEQ_1:26; reconsider y = y as Element of NAT by A124; x = q . y by A73, A124, A125; then A128: x = q /. y by A106, A124, A127, PARTFUN1:def_6; y <= len f by A126, FINSEQ_1:1; then A129: y < (len f) + 1 by NAT_1:13; x = q . ((len f) + 1) by A106, FINSEQ_1:42; then q /. y = q /. ((len f) + 1) by A106, A123, A128, PARTFUN1:def_6; hence contradiction by A69, A106, A124, A123, A127, A129; ::_thesis: verum end; A130: for z being set holds ( z in ((rng f) \/ {x}) \ {x} iff z in rng f ) proof let z be set ; ::_thesis: ( z in ((rng f) \/ {x}) \ {x} iff z in rng f ) hereby ::_thesis: ( z in rng f implies z in ((rng f) \/ {x}) \ {x} ) assume A131: z in ((rng f) \/ {x}) \ {x} ; ::_thesis: z in rng f then A132: not z in {x} by XBOOLE_0:def_5; z in (rng f) \/ {x} by A131, XBOOLE_0:def_5; hence z in rng f by A132, XBOOLE_0:def_3; ::_thesis: verum end; assume A133: z in rng f ; ::_thesis: z in ((rng f) \/ {x}) \ {x} then A134: z in (rng f) \/ {x} by XBOOLE_0:def_3; not z in {x} by A122, A133, TARSKI:def_1; hence z in ((rng f) \/ {x}) \ {x} by A134, XBOOLE_0:def_5; ::_thesis: verum end; rng (f ^ <*x*>) = (rng f) \/ (rng <*x*>) by FINSEQ_1:31 .= (rng f) \/ {x} by FINSEQ_1:39 ; hence rng f = rng p by A68, A106, A120, A130, TARSKI:1; ::_thesis: for l, m being Nat st l in dom f & m in dom f & l < m holds ( f /. l <> f /. m & [(f /. l),(f /. m)] in R ) let l, m be Nat; ::_thesis: ( l in dom f & m in dom f & l < m implies ( f /. l <> f /. m & [(f /. l),(f /. m)] in R ) ) assume that A135: l in dom f and A136: m in dom f and A137: l < m ; ::_thesis: ( f /. l <> f /. m & [(f /. l),(f /. m)] in R ) A138: f . m = f /. m by A136, PARTFUN1:def_6; A139: dom f c= dom q by A106, FINSEQ_1:26; then q . m = q /. m by A136, PARTFUN1:def_6; then A140: f /. m = q /. m by A73, A136, A138; A141: f . l = f /. l by A135, PARTFUN1:def_6; q . l = q /. l by A139, A135, PARTFUN1:def_6; then f /. l = q /. l by A73, A135, A141; hence ( f /. l <> f /. m & [(f /. l),(f /. m)] in R ) by A69, A139, A135, A136, A137, A140; ::_thesis: verum end; ( p is FinSequence of A9 & ( for l, m being Nat st l in dom p & m in dom p & l < m holds ( p /. l <> p /. m & [(p /. l),(p /. m)] in R ) ) ) proof thus p is FinSequence of A9 ; ::_thesis: for l, m being Nat st l in dom p & m in dom p & l < m holds ( p /. l <> p /. m & [(p /. l),(p /. m)] in R ) let l, m be Nat; ::_thesis: ( l in dom p & m in dom p & l < m implies ( p /. l <> p /. m & [(p /. l),(p /. m)] in R ) ) assume that A142: l in dom p and A143: m in dom p and A144: l < m ; ::_thesis: ( p /. l <> p /. m & [(p /. l),(p /. m)] in R ) A145: dom p c= dom (p ^ <*x*>) by FINSEQ_1:26; p . m = (p ^ <*x*>) . m by A143, FINSEQ_1:def_7; then p . m = (p ^ <*x*>) /. m by A143, A145, PARTFUN1:def_6; then A146: p /. m = (p ^ <*x*>) /. m by A143, PARTFUN1:def_6; p . l = (p ^ <*x*>) . l by A142, FINSEQ_1:def_7; then p . l = (p ^ <*x*>) /. l by A142, A145, PARTFUN1:def_6; then p /. l = (p ^ <*x*>) /. l by A142, PARTFUN1:def_6; hence ( p /. l <> p /. m & [(p /. l),(p /. m)] in R ) by A67, A142, A143, A144, A145, A146; ::_thesis: verum end; hence q = p ^ <*x*> by A66, A106, A121; ::_thesis: verum end; A147: now__::_thesis:_for_n,_m_being_Nat_st_n_in_dom_p_&_m_in_dom_p_&_n_<_m_holds_ (_p_/._n_<>_p_/._m_&_[(p_/._n),(p_/._m)]_in_R_) let n, m be Nat; ::_thesis: ( n in dom p & m in dom p & n < m implies ( p /. n <> p /. m & [(p /. n),(p /. m)] in R ) ) assume that A148: n in dom p and A149: m in dom p and A150: n < m ; ::_thesis: ( p /. n <> p /. m & [(p /. n),(p /. m)] in R ) A151: p /. m = p . m by A149, PARTFUN1:def_6 .= p9 /. m by A149, PARTFUN1:def_6 ; p /. n = p . n by A148, PARTFUN1:def_6 .= p9 /. n by A148, PARTFUN1:def_6 ; hence ( p /. n <> p /. m & [(p /. n),(p /. m)] in R ) by A60, A148, A149, A150, A151; ::_thesis: verum end; A152: now__::_thesis:_for_n,_m_being_Nat_st_n_in_dom_q_&_m_in_dom_q_&_n_<_m_holds_ (_q_/._n_<>_q_/._m_&_[(q_/._n),(q_/._m)]_in_R_) let n, m be Nat; ::_thesis: ( n in dom q & m in dom q & n < m implies ( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) ) assume that A153: n in dom q and A154: m in dom q and A155: n < m ; ::_thesis: ( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) A156: q /. m = q . m by A154, PARTFUN1:def_6 .= q9 /. m by A154, PARTFUN1:def_6 ; q /. n = q . n by A153, PARTFUN1:def_6 .= q9 /. n by A153, PARTFUN1:def_6 ; hence ( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) by A62, A153, A154, A155, A156; ::_thesis: verum end; A157: S1[ <*> A9] ; for p being FinSequence of A9 holds S1[p] from FINSEQ_2:sch_2(A157, A65); hence p9 = q9 by A59, A61, A147, A152; ::_thesis: verum end; end; end; end; :: deftheorem Def2 defines SgmX PRE_POLY:def_2_:_ for X being set for A being finite Subset of X for R being Order of X st R linearly_orders A holds for b4 being FinSequence of X holds ( b4 = SgmX (R,A) iff ( rng b4 = A & ( for n, m being Nat st n in dom b4 & m in dom b4 & n < m holds ( b4 /. n <> b4 /. m & [(b4 /. n),(b4 /. m)] in R ) ) ) ); theorem :: PRE_POLY:9 for X being set for A being finite Subset of X for R being Order of X for f being FinSequence of X st rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds ( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) holds f = SgmX (R,A) proof let X be set ; ::_thesis: for A being finite Subset of X for R being Order of X for f being FinSequence of X st rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds ( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) holds f = SgmX (R,A) let A be finite Subset of X; ::_thesis: for R being Order of X for f being FinSequence of X st rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds ( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) holds f = SgmX (R,A) let R be Order of X; ::_thesis: for f being FinSequence of X st rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds ( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) holds f = SgmX (R,A) let f be FinSequence of X; ::_thesis: ( rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds ( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) implies f = SgmX (R,A) ) assume that A1: rng f = A and A2: for n, m being Nat st n in dom f & m in dom f & n < m holds ( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ; ::_thesis: f = SgmX (R,A) now__::_thesis:_for_a,_b_being_set_st_a_in_A_&_b_in_A_&_a_<>_b_&_not_[a,b]_in_R_holds_ [b,a]_in_R let a, b be set ; ::_thesis: ( a in A & b in A & a <> b & not [a,b] in R implies [b,a] in R ) assume that A3: a in A and A4: b in A and A5: a <> b ; ::_thesis: ( [a,b] in R or [b,a] in R ) consider n being Nat such that A6: n in dom f and A7: f . n = a by A1, A3, FINSEQ_2:10; consider m being Nat such that A8: m in dom f and A9: f . m = b by A1, A4, FINSEQ_2:10; A10: f /. m = f . m by A8, PARTFUN1:def_6; A11: f /. n = f . n by A6, PARTFUN1:def_6; now__::_thesis:_(_not_[a,b]_in_R_implies_[b,a]_in_R_) assume that A12: not [a,b] in R and A13: not [b,a] in R ; ::_thesis: contradiction percases ( n = m or n <> m ) ; suppose n = m ; ::_thesis: contradiction hence contradiction by A5, A7, A9; ::_thesis: verum end; supposeA14: n <> m ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( n > m or m > n ) by A14, XXREAL_0:1; suppose n > m ; ::_thesis: contradiction hence contradiction by A2, A6, A7, A8, A9, A11, A10, A13; ::_thesis: verum end; suppose m > n ; ::_thesis: contradiction hence contradiction by A2, A6, A7, A8, A9, A11, A10, A12; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence ( [a,b] in R or [b,a] in R ) ; ::_thesis: verum end; then A15: R is_connected_in A by RELAT_2:def_6; A16: field R = X by ORDERS_1:12; then R is_antisymmetric_in X by RELAT_2:def_12; then A17: R is_antisymmetric_in A by ORDERS_1:9; R is_transitive_in X by A16, RELAT_2:def_16; then A18: R is_transitive_in A by ORDERS_1:10; R is_reflexive_in X by A16, RELAT_2:def_9; then R is_reflexive_in A by ORDERS_1:8; then R linearly_orders A by A17, A18, A15, ORDERS_1:def_8; hence f = SgmX (R,A) by A1, A2, Def2; ::_thesis: verum end; registration let X be set ; let F be non empty Subset of (Fin X); cluster -> finite for Element of F; coherence for b1 being Element of F holds b1 is finite ; end; definition let X be set ; let F be non empty Subset of (Fin X); :: original: Element redefine mode Element of F -> Subset of X; coherence for b1 being Element of F holds b1 is Subset of X proof let a be Element of F; ::_thesis: a is Subset of X thus a is Subset of X by FINSUB_1:17; ::_thesis: verum end; end; theorem Th10: :: PRE_POLY:10 for X being set for A being finite Subset of X for R being Order of X st R linearly_orders A holds SgmX (R,A) is one-to-one proof let X be set ; ::_thesis: for A being finite Subset of X for R being Order of X st R linearly_orders A holds SgmX (R,A) is one-to-one let A be finite Subset of X; ::_thesis: for R being Order of X st R linearly_orders A holds SgmX (R,A) is one-to-one let R be Order of X; ::_thesis: ( R linearly_orders A implies SgmX (R,A) is one-to-one ) set f = SgmX (R,A); assume A1: R linearly_orders A ; ::_thesis: SgmX (R,A) is one-to-one then rng (SgmX (R,A)) = A by Def2; then reconsider f = SgmX (R,A) as FinSequence of A by FINSEQ_1:def_4; f is one-to-one proof let k, l be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not k in dom f or not l in dom f or not f . k = f . l or k = l ) assume that A2: k in dom f and A3: l in dom f and A4: f . k = f . l ; ::_thesis: k = l reconsider k = k, l = l as Element of NAT by A2, A3; reconsider fk = f . k as Element of A by A2, FINSEQ_2:11; reconsider fl = f . l as Element of A by A3, FINSEQ_2:11; A5: fl = f /. l by A3, PARTFUN1:def_6; A6: fk = f /. k by A2, PARTFUN1:def_6; now__::_thesis:_not_k_<>_l A7: f /. l = f . l by A3, PARTFUN1:def_6 .= (SgmX (R,A)) /. l by A3, PARTFUN1:def_6 ; A8: f /. k = f . k by A2, PARTFUN1:def_6 .= (SgmX (R,A)) /. k by A2, PARTFUN1:def_6 ; assume A9: k <> l ; ::_thesis: contradiction percases ( k < l or l < k ) by A9, XXREAL_0:1; suppose k < l ; ::_thesis: contradiction hence contradiction by A1, A2, A3, A4, A6, A5, A8, A7, Def2; ::_thesis: verum end; suppose l < k ; ::_thesis: contradiction hence contradiction by A1, A2, A3, A4, A6, A5, A8, A7, Def2; ::_thesis: verum end; end; end; hence k = l ; ::_thesis: verum end; hence SgmX (R,A) is one-to-one ; ::_thesis: verum end; theorem :: PRE_POLY:11 for X being set for A being finite Subset of X for R being Order of X st R linearly_orders A holds len (SgmX (R,A)) = card A proof let X be set ; ::_thesis: for A being finite Subset of X for R being Order of X st R linearly_orders A holds len (SgmX (R,A)) = card A let A be finite Subset of X; ::_thesis: for R being Order of X st R linearly_orders A holds len (SgmX (R,A)) = card A let R be Order of X; ::_thesis: ( R linearly_orders A implies len (SgmX (R,A)) = card A ) set f = SgmX (R,A); A1: dom (SgmX (R,A)) = Seg (len (SgmX (R,A))) by FINSEQ_1:def_3; Seg (len (SgmX (R,A))), len (SgmX (R,A)) are_equipotent by FINSEQ_1:54; then A2: card (Seg (len (SgmX (R,A)))) = card (len (SgmX (R,A))) by CARD_1:5; assume A3: R linearly_orders A ; ::_thesis: len (SgmX (R,A)) = card A then A4: SgmX (R,A) is one-to-one by Th10; rng (SgmX (R,A)) = A by A3, Def2; then Seg (len (SgmX (R,A))),A are_equipotent by A1, A4, WELLORD2:def_4; hence len (SgmX (R,A)) = card A by A2, CARD_1:5; ::_thesis: verum end; begin theorem Th12: :: PRE_POLY:12 for n being Nat for M being FinSequence st len M = n + 1 holds len (Del (M,(n + 1))) = n proof let n be Nat; ::_thesis: for M being FinSequence st len M = n + 1 holds len (Del (M,(n + 1))) = n let M be FinSequence; ::_thesis: ( len M = n + 1 implies len (Del (M,(n + 1))) = n ) assume A1: len M = n + 1 ; ::_thesis: len (Del (M,(n + 1))) = n then n + 1 in Seg (len M) by FINSEQ_1:4; then n + 1 in dom M by FINSEQ_1:def_3; hence len (Del (M,(n + 1))) = n by A1, FINSEQ_3:109; ::_thesis: verum end; theorem :: PRE_POLY:13 for n being Nat for M being FinSequence st len M = n + 1 holds M = (Del (M,(len M))) ^ <*(M . (len M))*> proof let n be Nat; ::_thesis: for M being FinSequence st len M = n + 1 holds M = (Del (M,(len M))) ^ <*(M . (len M))*> let M be FinSequence; ::_thesis: ( len M = n + 1 implies M = (Del (M,(len M))) ^ <*(M . (len M))*> ) assume len M = n + 1 ; ::_thesis: M = (Del (M,(len M))) ^ <*(M . (len M))*> then M <> {} ; then consider q being FinSequence, x being set such that A1: M = q ^ <*x*> by FINSEQ_1:46; A2: len M = (len q) + (len <*x*>) by A1, FINSEQ_1:22 .= (len q) + 1 by FINSEQ_1:39 ; then A3: len (Del (M,(len M))) = len q by Th12; A4: dom q = Seg (len q) by FINSEQ_1:def_3; A5: now__::_thesis:_for_i_being_Nat_st_i_in_dom_q_holds_ (Del_(M,(len_M)))_._i_=_q_._i let i be Nat; ::_thesis: ( i in dom q implies (Del (M,(len M))) . i = q . i ) assume A6: i in dom q ; ::_thesis: (Del (M,(len M))) . i = q . i then i <= len q by A4, FINSEQ_1:1; then ( i in NAT & i < len M ) by A2, NAT_1:13, ORDINAL1:def_12; hence (Del (M,(len M))) . i = M . i by FINSEQ_3:110 .= q . i by A1, A6, FINSEQ_1:def_7 ; ::_thesis: verum end; M . (len M) = x by A1, A2, FINSEQ_1:42; hence M = (Del (M,(len M))) ^ <*(M . (len M))*> by A1, A3, A5, FINSEQ_2:9; ::_thesis: verum end; definition let IT be Function; attrIT is FinSequence-yielding means :Def3: :: PRE_POLY:def 3 for x being set st x in dom IT holds IT . x is FinSequence; end; :: deftheorem Def3 defines FinSequence-yielding PRE_POLY:def_3_:_ for IT being Function holds ( IT is FinSequence-yielding iff for x being set st x in dom IT holds IT . x is FinSequence ); registration cluster Relation-like Function-like FinSequence-yielding for set ; existence ex b1 being Function st b1 is FinSequence-yielding proof set f = the FinSequence; set I = the set ; take F = the set --> the FinSequence; ::_thesis: F is FinSequence-yielding let x be set ; :: according to PRE_POLY:def_3 ::_thesis: ( x in dom F implies F . x is FinSequence ) assume x in dom F ; ::_thesis: F . x is FinSequence hence F . x is FinSequence by FUNCOP_1:7; ::_thesis: verum end; end; definition let F, G be FinSequence-yielding Function; funcF ^^ G -> FinSequence-yielding Function means :Def4: :: PRE_POLY:def 4 ( dom it = (dom F) /\ (dom G) & ( for i being set st i in dom it holds for f, g being FinSequence st f = F . i & g = G . i holds it . i = f ^ g ) ); existence ex b1 being FinSequence-yielding Function st ( dom b1 = (dom F) /\ (dom G) & ( for i being set st i in dom b1 holds for f, g being FinSequence st f = F . i & g = G . i holds b1 . i = f ^ g ) ) proof defpred S1[ set , set ] means for f, g being FinSequence st f = F . $1 & g = G . $1 holds $2 = f ^ g; A1: for i being set st i in (dom F) /\ (dom G) holds ex u being set st S1[i,u] proof let i be set ; ::_thesis: ( i in (dom F) /\ (dom G) implies ex u being set st S1[i,u] ) assume i in (dom F) /\ (dom G) ; ::_thesis: ex u being set st S1[i,u] then ( i in dom F & i in dom G ) by XBOOLE_0:def_4; then reconsider f = F . i, g = G . i as FinSequence by Def3; take f ^ g ; ::_thesis: S1[i,f ^ g] thus S1[i,f ^ g] ; ::_thesis: verum end; consider H being Function such that A2: ( dom H = (dom F) /\ (dom G) & ( for i being set st i in (dom F) /\ (dom G) holds S1[i,H . i] ) ) from CLASSES1:sch_1(A1); for x being set st x in dom H holds H . x is FinSequence proof let x be set ; ::_thesis: ( x in dom H implies H . x is FinSequence ) assume A3: x in dom H ; ::_thesis: H . x is FinSequence then x in dom F by A2, XBOOLE_0:def_4; then reconsider f = F . x as FinSequence by Def3; x in dom G by A2, A3, XBOOLE_0:def_4; then reconsider g = G . x as FinSequence by Def3; H . x = f ^ g by A2, A3; hence H . x is FinSequence ; ::_thesis: verum end; then reconsider H = H as FinSequence-yielding Function by Def3; take H ; ::_thesis: ( dom H = (dom F) /\ (dom G) & ( for i being set st i in dom H holds for f, g being FinSequence st f = F . i & g = G . i holds H . i = f ^ g ) ) thus ( dom H = (dom F) /\ (dom G) & ( for i being set st i in dom H holds for f, g being FinSequence st f = F . i & g = G . i holds H . i = f ^ g ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence-yielding Function st dom b1 = (dom F) /\ (dom G) & ( for i being set st i in dom b1 holds for f, g being FinSequence st f = F . i & g = G . i holds b1 . i = f ^ g ) & dom b2 = (dom F) /\ (dom G) & ( for i being set st i in dom b2 holds for f, g being FinSequence st f = F . i & g = G . i holds b2 . i = f ^ g ) holds b1 = b2 proof let F1, F2 be FinSequence-yielding Function; ::_thesis: ( dom F1 = (dom F) /\ (dom G) & ( for i being set st i in dom F1 holds for f, g being FinSequence st f = F . i & g = G . i holds F1 . i = f ^ g ) & dom F2 = (dom F) /\ (dom G) & ( for i being set st i in dom F2 holds for f, g being FinSequence st f = F . i & g = G . i holds F2 . i = f ^ g ) implies F1 = F2 ) assume that A4: dom F1 = (dom F) /\ (dom G) and A5: for i being set st i in dom F1 holds for f, g being FinSequence st f = F . i & g = G . i holds F1 . i = f ^ g and A6: dom F2 = (dom F) /\ (dom G) and A7: for i being set st i in dom F2 holds for f, g being FinSequence st f = F . i & g = G . i holds F2 . i = f ^ g ; ::_thesis: F1 = F2 now__::_thesis:_for_x_being_set_st_x_in_dom_F1_holds_ F1_._x_=_F2_._x let x be set ; ::_thesis: ( x in dom F1 implies F1 . x = F2 . x ) assume A8: x in dom F1 ; ::_thesis: F1 . x = F2 . x then ( x in dom F & x in dom G ) by A4, XBOOLE_0:def_4; then reconsider f = F . x, g = G . x as FinSequence by Def3; thus F1 . x = f ^ g by A5, A8 .= F2 . x by A4, A6, A7, A8 ; ::_thesis: verum end; hence F1 = F2 by A4, A6, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def4 defines ^^ PRE_POLY:def_4_:_ for F, G, b3 being FinSequence-yielding Function holds ( b3 = F ^^ G iff ( dom b3 = (dom F) /\ (dom G) & ( for i being set st i in dom b3 holds for f, g being FinSequence st f = F . i & g = G . i holds b3 . i = f ^ g ) ) ); begin theorem :: PRE_POLY:14 for V, C being non empty set ex f being Element of PFuncs (V,C) st f <> {} proof let V, C be non empty set ; ::_thesis: ex f being Element of PFuncs (V,C) st f <> {} consider a being set such that A1: a in V by XBOOLE_0:def_1; consider b being set such that A2: b in C by XBOOLE_0:def_1; set f = {[a,b]}; {a} c= V by A1, ZFMISC_1:31; then A3: dom {[a,b]} c= V by RELAT_1:9; {b} c= C by A2, ZFMISC_1:31; then rng {[a,b]} c= C by RELAT_1:9; then reconsider f = {[a,b]} as Element of PFuncs (V,C) by A3, PARTFUN1:def_3; f <> {} ; hence ex f being Element of PFuncs (V,C) st f <> {} ; ::_thesis: verum end; theorem :: PRE_POLY:15 for V, C being set for f being Element of PFuncs (V,C) for g being set st g c= f holds g in PFuncs (V,C) proof let V, C be set ; ::_thesis: for f being Element of PFuncs (V,C) for g being set st g c= f holds g in PFuncs (V,C) let f be Element of PFuncs (V,C); ::_thesis: for g being set st g c= f holds g in PFuncs (V,C) let g be set ; ::_thesis: ( g c= f implies g in PFuncs (V,C) ) consider f1 being Function such that A1: f1 = f and A2: dom f1 c= V and A3: rng f1 c= C by PARTFUN1:def_3; assume A4: g c= f ; ::_thesis: g in PFuncs (V,C) then reconsider g9 = g as Function ; rng g9 c= rng f1 by A4, A1, RELAT_1:11; then A5: rng g9 c= C by A3, XBOOLE_1:1; dom g9 c= dom f1 by A4, A1, RELAT_1:11; then dom g9 c= V by A2, XBOOLE_1:1; hence g in PFuncs (V,C) by A5, PARTFUN1:def_3; ::_thesis: verum end; theorem Th16: :: PRE_POLY:16 for V, C being set holds PFuncs (V,C) c= bool [:V,C:] proof let V, C be set ; ::_thesis: PFuncs (V,C) c= bool [:V,C:] let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PFuncs (V,C) or x in bool [:V,C:] ) assume x in PFuncs (V,C) ; ::_thesis: x in bool [:V,C:] then consider f being Function such that A1: x = f and A2: dom f c= V and A3: rng f c= C by PARTFUN1:def_3; A4: f c= [:(dom f),(rng f):] by RELAT_1:7; [:(dom f),(rng f):] c= [:V,C:] by A2, A3, ZFMISC_1:96; then f c= [:V,C:] by A4, XBOOLE_1:1; hence x in bool [:V,C:] by A1; ::_thesis: verum end; theorem Th17: :: PRE_POLY:17 for V, C being set st V is finite & C is finite holds PFuncs (V,C) is finite proof let V, C be set ; ::_thesis: ( V is finite & C is finite implies PFuncs (V,C) is finite ) assume that A1: V is finite and A2: C is finite ; ::_thesis: PFuncs (V,C) is finite PFuncs (V,C) c= bool [:V,C:] by Th16; hence PFuncs (V,C) is finite by A1, A2; ::_thesis: verum end; registration cluster functional non empty finite for set ; existence ex b1 being set st ( b1 is functional & b1 is finite & not b1 is empty ) proof set A = the non empty finite set ; take P = PFuncs ( the non empty finite set , the non empty finite set ); ::_thesis: ( P is functional & P is finite & not P is empty ) thus P is functional ; ::_thesis: ( P is finite & not P is empty ) thus P is finite by Th17; ::_thesis: not P is empty thus not P is empty ; ::_thesis: verum end; end; begin registration let D be set ; cluster -> FinSequence-yielding for FinSequence of D * ; coherence for b1 being FinSequence of D * holds b1 is FinSequence-yielding proof let f be FinSequence of D * ; ::_thesis: f is FinSequence-yielding let x be set ; :: according to PRE_POLY:def_3 ::_thesis: ( x in dom f implies f . x is FinSequence ) assume x in dom f ; ::_thesis: f . x is FinSequence then reconsider x = x as Element of NAT ; thus f . x is FinSequence ; ::_thesis: verum end; end; registration cluster Relation-like Function-like FinSequence-yielding -> Function-yielding for set ; coherence for b1 being Function st b1 is FinSequence-yielding holds b1 is Function-yielding proof let f be Function; ::_thesis: ( f is FinSequence-yielding implies f is Function-yielding ) assume A1: f is FinSequence-yielding ; ::_thesis: f is Function-yielding let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in dom f or f . x is set ) thus ( not x in dom f or f . x is set ) by A1, Def3; ::_thesis: verum end; end; begin theorem Th18: :: PRE_POLY:18 for X being set for R being Relation st field R c= X holds R is Relation of X proof let X be set ; ::_thesis: for R being Relation st field R c= X holds R is Relation of X let R be Relation; ::_thesis: ( field R c= X implies R is Relation of X ) assume A1: field R c= X ; ::_thesis: R is Relation of X R c= [:X,X:] proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in R or [x,y] in [:X,X:] ) assume [x,y] in R ; ::_thesis: [x,y] in [:X,X:] then ( x in field R & y in field R ) by RELAT_1:15; hence [x,y] in [:X,X:] by A1, ZFMISC_1:def_2; ::_thesis: verum end; hence R is Relation of X ; ::_thesis: verum end; registration let X be set ; let f be ManySortedSet of X; let x, y be set ; clusterf +* (x,y) -> X -defined ; coherence f +* (x,y) is X -defined proof dom (f +* (x,y)) = dom f by FUNCT_7:30 .= X by PARTFUN1:def_2 ; hence f +* (x,y) is X -defined by RELAT_1:def_18; ::_thesis: verum end; end; registration let X be set ; let f be ManySortedSet of X; let x, y be set ; clusterf +* (x,y) -> X -defined total for X -defined Function; coherence for b1 being X -defined Function st b1 = f +* (x,y) holds b1 is total proof dom (f +* (x,y)) = dom f by FUNCT_7:30 .= X by PARTFUN1:def_2 ; hence for b1 being X -defined Function st b1 = f +* (x,y) holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; end; theorem Th19: :: PRE_POLY:19 for f being one-to-one Function holds card f = card (rng f) proof let f be one-to-one Function; ::_thesis: card f = card (rng f) A1: ( rng f = dom (f ") & dom f = rng (f ") ) by FUNCT_1:33; ( card (rng f) c= card (dom f) & card (rng (f ")) c= card (dom (f ")) ) by CARD_2:61; then card (rng f) = card (dom f) by A1, XBOOLE_0:def_10; hence card f = card (rng f) by CARD_1:62; ::_thesis: verum end; definition let A, X be set ; let D be non empty FinSequenceSet of A; let p be PartFunc of X,D; let i be set ; :: original: /. redefine funcp /. i -> Element of D; coherence p /. i is Element of D ; end; registration let X be set ; cluster Relation-like X -defined X -valued total quasi_total reflexive antisymmetric transitive well-ordering being_linear-order for Element of bool [:X,X:]; existence ex b1 being Order of X st ( b1 is being_linear-order & b1 is well-ordering ) proof consider R being Relation such that A1: R is well-ordering and A2: field R = X by WELLSET1:6; reconsider R = R as Relation of X by A2, Th18; A3: R is connected by A1, WELLORD1:def_4; R is reflexive by A1, WELLORD1:def_4; then R is_reflexive_in X by A2, RELAT_2:def_9; then dom R = X by ORDERS_1:13; then reconsider R = R as Order of X by A1, PARTFUN1:def_2, WELLORD1:def_4; take R ; ::_thesis: ( R is being_linear-order & R is well-ordering ) thus ( R is being_linear-order & R is well-ordering ) by A1, A3, ORDERS_1:def_5; ::_thesis: verum end; end; theorem Th20: :: PRE_POLY:20 for X being non empty set for A being non empty finite Subset of X for R being Order of X for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds [x,y] in R ) holds (SgmX (R,A)) /. 1 = x proof let X be non empty set ; ::_thesis: for A being non empty finite Subset of X for R being Order of X for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds [x,y] in R ) holds (SgmX (R,A)) /. 1 = x let A be non empty finite Subset of X; ::_thesis: for R being Order of X for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds [x,y] in R ) holds (SgmX (R,A)) /. 1 = x let R be Order of X; ::_thesis: for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds [x,y] in R ) holds (SgmX (R,A)) /. 1 = x let x be Element of X; ::_thesis: ( x in A & R linearly_orders A & ( for y being Element of X st y in A holds [x,y] in R ) implies (SgmX (R,A)) /. 1 = x ) assume that A1: x in A and A2: R linearly_orders A and A3: for y being Element of X st y in A holds [x,y] in R and A4: (SgmX (R,A)) /. 1 <> x ; ::_thesis: contradiction A5: A = rng (SgmX (R,A)) by A2, Def2; then consider i being Element of NAT such that A6: i in dom (SgmX (R,A)) and A7: (SgmX (R,A)) /. i = x by A1, PARTFUN2:2; not SgmX (R,A) is empty by A2, Def2, RELAT_1:38; then A8: 1 in dom (SgmX (R,A)) by FINSEQ_5:6; then (SgmX (R,A)) /. 1 in A by A5, PARTFUN2:2; then A9: [x,((SgmX (R,A)) /. 1)] in R by A3; field R = X by ORDERS_1:12; then A10: R is_antisymmetric_in X by RELAT_2:def_12; 1 <= i by A6, FINSEQ_3:25; then 1 < i by A4, A7, XXREAL_0:1; then [((SgmX (R,A)) /. 1),x] in R by A2, A6, A7, A8, Def2; hence contradiction by A4, A9, A10, RELAT_2:def_4; ::_thesis: verum end; theorem Th21: :: PRE_POLY:21 for X being non empty set for A being non empty finite Subset of X for R being Order of X for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds [y,x] in R ) holds (SgmX (R,A)) /. (len (SgmX (R,A))) = x proof let X be non empty set ; ::_thesis: for A being non empty finite Subset of X for R being Order of X for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds [y,x] in R ) holds (SgmX (R,A)) /. (len (SgmX (R,A))) = x let A be non empty finite Subset of X; ::_thesis: for R being Order of X for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds [y,x] in R ) holds (SgmX (R,A)) /. (len (SgmX (R,A))) = x let R be Order of X; ::_thesis: for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds [y,x] in R ) holds (SgmX (R,A)) /. (len (SgmX (R,A))) = x let x be Element of X; ::_thesis: ( x in A & R linearly_orders A & ( for y being Element of X st y in A holds [y,x] in R ) implies (SgmX (R,A)) /. (len (SgmX (R,A))) = x ) assume that A1: x in A and A2: R linearly_orders A and A3: for y being Element of X st y in A holds [y,x] in R and A4: (SgmX (R,A)) /. (len (SgmX (R,A))) <> x ; ::_thesis: contradiction set L = len (SgmX (R,A)); A5: A = rng (SgmX (R,A)) by A2, Def2; then consider i being Element of NAT such that A6: i in dom (SgmX (R,A)) and A7: (SgmX (R,A)) /. i = x by A1, PARTFUN2:2; not SgmX (R,A) is empty by A2, Def2, RELAT_1:38; then A8: len (SgmX (R,A)) in dom (SgmX (R,A)) by FINSEQ_5:6; then (SgmX (R,A)) /. (len (SgmX (R,A))) in A by A5, PARTFUN2:2; then A9: [((SgmX (R,A)) /. (len (SgmX (R,A)))),x] in R by A3; field R = X by ORDERS_1:12; then A10: R is_antisymmetric_in X by RELAT_2:def_12; i <= len (SgmX (R,A)) by A6, FINSEQ_3:25; then i < len (SgmX (R,A)) by A4, A7, XXREAL_0:1; then [x,((SgmX (R,A)) /. (len (SgmX (R,A))))] in R by A2, A6, A7, A8, Def2; hence contradiction by A4, A9, A10, RELAT_2:def_4; ::_thesis: verum end; registration let X be non empty set ; let A be non empty finite Subset of X; let R be being_linear-order Order of X; cluster SgmX (R,A) -> one-to-one non empty ; coherence ( not SgmX (R,A) is empty & SgmX (R,A) is one-to-one ) proof field R = X by ORDERS_1:15; then R linearly_orders A by ORDERS_1:37, ORDERS_1:38; hence ( not SgmX (R,A) is empty & SgmX (R,A) is one-to-one ) by Th10, Def2, RELAT_1:38; ::_thesis: verum end; end; registration cluster Relation-like Function-like empty -> FinSequence-yielding for set ; coherence for b1 being Function st b1 is empty holds b1 is FinSequence-yielding proof let F be Function; ::_thesis: ( F is empty implies F is FinSequence-yielding ) assume A1: F is empty ; ::_thesis: F is FinSequence-yielding let x be set ; :: according to PRE_POLY:def_3 ::_thesis: ( x in dom F implies F . x is FinSequence ) thus ( x in dom F implies F . x is FinSequence ) by A1; ::_thesis: verum end; end; registration let F, G be FinSequence-yielding FinSequence; clusterF ^^ G -> FinSequence-like FinSequence-yielding ; coherence F ^^ G is FinSequence-like proof dom (F ^^ G) = (dom F) /\ (dom G) by Def4 .= (Seg (len F)) /\ (dom G) by FINSEQ_1:def_3 .= (Seg (len F)) /\ (Seg (len G)) by FINSEQ_1:def_3 .= Seg (min ((len F),(len G))) by FINSEQ_2:2 ; hence F ^^ G is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum end; end; registration let i be Element of NAT ; let f be FinSequence; clusteri |-> f -> FinSequence-yielding ; coherence i |-> f is FinSequence-yielding proof let x be set ; :: according to PRE_POLY:def_3 ::_thesis: ( x in dom (i |-> f) implies (i |-> f) . x is FinSequence ) assume x in dom (i |-> f) ; ::_thesis: (i |-> f) . x is FinSequence then x in Seg i by FUNCOP_1:13; hence (i |-> f) . x is FinSequence by FUNCOP_1:7; ::_thesis: verum end; end; registration let F be FinSequence-yielding FinSequence; let x be set ; clusterF . x -> FinSequence-like ; coherence F . x is FinSequence-like proof percases ( not x in dom F or x in dom F ) ; suppose not x in dom F ; ::_thesis: F . x is FinSequence-like hence F . x is FinSequence-like by FUNCT_1:def_2; ::_thesis: verum end; suppose x in dom F ; ::_thesis: F . x is FinSequence-like hence F . x is FinSequence-like by Def3; ::_thesis: verum end; end; end; end; registration let F be FinSequence; cluster Card F -> FinSequence-like ; coherence Card F is FinSequence-like proof dom (Card F) = dom F by CARD_3:def_2 .= Seg (len F) by FINSEQ_1:def_3 ; hence Card F is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum end; end; registration cluster Relation-like NAT -defined Function-like finite Cardinal-yielding countable FinSequence-like FinSubsequence-like for set ; existence ex b1 being FinSequence st b1 is Cardinal-yielding proof take {} ; ::_thesis: {} is Cardinal-yielding thus {} is Cardinal-yielding ; ::_thesis: verum end; end; theorem Th22: :: PRE_POLY:22 for f being Function holds ( f is Cardinal-yielding iff for y being set st y in rng f holds y is Cardinal ) proof let f be Function; ::_thesis: ( f is Cardinal-yielding iff for y being set st y in rng f holds y is Cardinal ) hereby ::_thesis: ( ( for y being set st y in rng f holds y is Cardinal ) implies f is Cardinal-yielding ) assume A1: f is Cardinal-yielding ; ::_thesis: for y being set st y in rng f holds y is Cardinal let y be set ; ::_thesis: ( y in rng f implies y is Cardinal ) assume y in rng f ; ::_thesis: y is Cardinal then ex x being set st ( x in dom f & y = f . x ) by FUNCT_1:def_3; hence y is Cardinal by A1, CARD_3:def_1; ::_thesis: verum end; assume A2: for y being set st y in rng f holds y is Cardinal ; ::_thesis: f is Cardinal-yielding let x be set ; :: according to CARD_3:def_1 ::_thesis: ( not x in dom f or f . x is set ) assume x in dom f ; ::_thesis: f . x is set then f . x in rng f by FUNCT_1:def_3; hence f . x is set by A2; ::_thesis: verum end; registration let F, G be Cardinal-yielding FinSequence; clusterF ^ G -> Cardinal-yielding ; coherence F ^ G is Cardinal-yielding proof A1: rng (F ^ G) = (rng F) \/ (rng G) by FINSEQ_1:31; now__::_thesis:_for_y_being_set_st_y_in_rng_(F_^_G)_holds_ y_is_Cardinal let y be set ; ::_thesis: ( y in rng (F ^ G) implies y is Cardinal ) assume y in rng (F ^ G) ; ::_thesis: y is Cardinal then ( y in rng F or y in rng G ) by A1, XBOOLE_0:def_3; hence y is Cardinal by Th22; ::_thesis: verum end; hence F ^ G is Cardinal-yielding by Th22; ::_thesis: verum end; end; registration cluster -> Cardinal-yielding for FinSequence of NAT ; coherence for b1 being FinSequence of NAT holds b1 is Cardinal-yielding proof let f be FinSequence of NAT ; ::_thesis: f is Cardinal-yielding let x be set ; :: according to CARD_3:def_1 ::_thesis: ( not x in dom f or f . x is set ) assume x in dom f ; ::_thesis: f . x is set thus f . x is set ; ::_thesis: verum end; end; registration cluster Relation-like NAT -defined NAT -valued Function-like finite Cardinal-yielding countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued for FinSequence of NAT ; existence ex b1 being FinSequence of NAT st b1 is Cardinal-yielding proof take <*> NAT ; ::_thesis: <*> NAT is Cardinal-yielding thus <*> NAT is Cardinal-yielding ; ::_thesis: verum end; end; definition let D be set ; let F be FinSequence of D * ; :: original: Card redefine func Card F -> Cardinal-yielding FinSequence of NAT ; coherence Card F is Cardinal-yielding FinSequence of NAT proof rng (Card F) c= NAT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (Card F) or y in NAT ) assume y in rng (Card F) ; ::_thesis: y in NAT then consider x being set such that A1: x in dom (Card F) and A2: y = (Card F) . x by FUNCT_1:def_3; reconsider Fx = F . x as finite set ; x in dom F by A1, CARD_3:def_2; then y = card Fx by A2, CARD_3:def_2; hence y in NAT ; ::_thesis: verum end; hence Card F is Cardinal-yielding FinSequence of NAT by FINSEQ_1:def_4; ::_thesis: verum end; end; registration let F be FinSequence of NAT ; let i be Element of NAT ; clusterF | i -> Cardinal-yielding ; coherence F | i is Cardinal-yielding ; end; theorem Th23: :: PRE_POLY:23 for F being Function for X being set holds Card (F | X) = (Card F) | X proof let F be Function; ::_thesis: for X being set holds Card (F | X) = (Card F) | X let X be set ; ::_thesis: Card (F | X) = (Card F) | X A1: dom ((Card F) | X) = (dom (Card F)) /\ X by RELAT_1:61 .= (dom F) /\ X by CARD_3:def_2 .= dom (F | X) by RELAT_1:61 ; now__::_thesis:_for_x_being_set_st_x_in_dom_(F_|_X)_holds_ ((Card_F)_|_X)_._x_=_card_((F_|_X)_._x) let x be set ; ::_thesis: ( x in dom (F | X) implies ((Card F) | X) . x = card ((F | X) . x) ) A2: dom (F | X) c= dom F by RELAT_1:60; assume A3: x in dom (F | X) ; ::_thesis: ((Card F) | X) . x = card ((F | X) . x) hence ((Card F) | X) . x = (Card F) . x by A1, FUNCT_1:47 .= card (F . x) by A3, A2, CARD_3:def_2 .= card ((F | X) . x) by A3, FUNCT_1:47 ; ::_thesis: verum end; hence Card (F | X) = (Card F) | X by A1, CARD_3:def_2; ::_thesis: verum end; registration let F be empty Function; cluster Card F -> empty ; coherence Card F is empty proof dom F is empty ; then dom (Card F) is empty by CARD_3:def_2; hence Card F is empty ; ::_thesis: verum end; end; theorem Th24: :: PRE_POLY:24 for p being set holds Card <*p*> = <*(card p)*> proof let p be set ; ::_thesis: Card <*p*> = <*(card p)*> set Cp = <*(card p)*>; A1: dom <*(card p)*> = {1} by FINSEQ_1:2, FINSEQ_1:38; now__::_thesis:_for_x_being_set_st_x_in_dom_<*(card_p)*>_holds_ <*(card_p)*>_._x_is_Cardinal let x be set ; ::_thesis: ( x in dom <*(card p)*> implies <*(card p)*> . x is Cardinal ) assume x in dom <*(card p)*> ; ::_thesis: <*(card p)*> . x is Cardinal then x = 1 by A1, TARSKI:def_1; hence <*(card p)*> . x is Cardinal by FINSEQ_1:40; ::_thesis: verum end; then reconsider Cp = <*(card p)*> as Cardinal-Function by CARD_3:def_1; A2: dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38; now__::_thesis:_for_x_being_set_st_x_in_dom_<*p*>_holds_ <*(card_p)*>_._x_=_card_(<*p*>_._x) let x be set ; ::_thesis: ( x in dom <*p*> implies <*(card p)*> . x = card (<*p*> . x) ) assume x in dom <*p*> ; ::_thesis: <*(card p)*> . x = card (<*p*> . x) then A3: x = 1 by A2, TARSKI:def_1; hence <*(card p)*> . x = card p by FINSEQ_1:40 .= card (<*p*> . x) by A3, FINSEQ_1:40 ; ::_thesis: verum end; then Card <*p*> = Cp by A1, A2, CARD_3:def_2; hence Card <*p*> = <*(card p)*> ; ::_thesis: verum end; theorem Th25: :: PRE_POLY:25 for F, G being FinSequence holds Card (F ^ G) = (Card F) ^ (Card G) proof let F, G be FinSequence; ::_thesis: Card (F ^ G) = (Card F) ^ (Card G) A1: dom (Card G) = dom G by CARD_3:def_2; then A2: len (Card G) = len G by FINSEQ_3:29; A3: dom (Card F) = dom F by CARD_3:def_2; then A4: len (Card F) = len F by FINSEQ_3:29; A5: now__::_thesis:_for_x_being_set_st_x_in_dom_(F_^_G)_holds_ ((Card_F)_^_(Card_G))_._x_=_card_((F_^_G)_._x) let x be set ; ::_thesis: ( x in dom (F ^ G) implies ((Card F) ^ (Card G)) . b1 = card ((F ^ G) . b1) ) assume A6: x in dom (F ^ G) ; ::_thesis: ((Card F) ^ (Card G)) . b1 = card ((F ^ G) . b1) then reconsider k = x as Element of NAT ; x in Seg ((len F) + (len G)) by A6, FINSEQ_1:def_7; then A7: 1 <= k by FINSEQ_1:1; percases ( k <= len F or len F < k ) ; suppose k <= len F ; ::_thesis: ((Card F) ^ (Card G)) . b1 = card ((F ^ G) . b1) then A8: k in dom F by A7, FINSEQ_3:25; hence ((Card F) ^ (Card G)) . x = (Card F) . k by A3, FINSEQ_1:def_7 .= card (F . k) by A8, CARD_3:def_2 .= card ((F ^ G) . x) by A8, FINSEQ_1:def_7 ; ::_thesis: verum end; suppose len F < k ; ::_thesis: ((Card F) ^ (Card G)) . b1 = card ((F ^ G) . b1) then not k in dom F by FINSEQ_3:25; then consider n being Nat such that A9: n in dom G and A10: k = (len F) + n by A6, FINSEQ_1:25; thus ((Card F) ^ (Card G)) . x = (Card G) . n by A1, A4, A9, A10, FINSEQ_1:def_7 .= card (G . n) by A9, CARD_3:def_2 .= card ((F ^ G) . x) by A9, A10, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; dom ((Card F) ^ (Card G)) = Seg ((len (Card F)) + (len (Card G))) by FINSEQ_1:def_7 .= dom (F ^ G) by A4, A2, FINSEQ_1:def_7 ; hence Card (F ^ G) = (Card F) ^ (Card G) by A5, CARD_3:def_2; ::_thesis: verum end; registration let X be set ; cluster <*> X -> FinSequence-yielding ; coherence <*> X is FinSequence-yielding ; end; registration let f be FinSequence; cluster<*f*> -> FinSequence-yielding ; coherence <*f*> is FinSequence-yielding proof let x be set ; :: according to PRE_POLY:def_3 ::_thesis: ( x in dom <*f*> implies <*f*> . x is FinSequence ) assume x in dom <*f*> ; ::_thesis: <*f*> . x is FinSequence then x in {1} by FINSEQ_1:2, FINSEQ_1:38; then x = 1 by TARSKI:def_1; hence <*f*> . x is FinSequence by FINSEQ_1:40; ::_thesis: verum end; end; theorem Th26: :: PRE_POLY:26 for f being Function holds ( f is FinSequence-yielding iff for y being set st y in rng f holds y is FinSequence ) proof let f be Function; ::_thesis: ( f is FinSequence-yielding iff for y being set st y in rng f holds y is FinSequence ) hereby ::_thesis: ( ( for y being set st y in rng f holds y is FinSequence ) implies f is FinSequence-yielding ) assume A1: f is FinSequence-yielding ; ::_thesis: for y being set st y in rng f holds y is FinSequence let y be set ; ::_thesis: ( y in rng f implies y is FinSequence ) assume y in rng f ; ::_thesis: y is FinSequence then ex x being set st ( x in dom f & y = f . x ) by FUNCT_1:def_3; hence y is FinSequence by A1, Def3; ::_thesis: verum end; assume A2: for y being set st y in rng f holds y is FinSequence ; ::_thesis: f is FinSequence-yielding let x be set ; :: according to PRE_POLY:def_3 ::_thesis: ( x in dom f implies f . x is FinSequence ) assume x in dom f ; ::_thesis: f . x is FinSequence then f . x in rng f by FUNCT_1:def_3; hence f . x is FinSequence by A2; ::_thesis: verum end; registration let F, G be FinSequence-yielding FinSequence; clusterF ^ G -> FinSequence-yielding ; coherence F ^ G is FinSequence-yielding proof A1: rng (F ^ G) = (rng F) \/ (rng G) by FINSEQ_1:31; now__::_thesis:_for_y_being_set_st_y_in_rng_(F_^_G)_holds_ y_is_FinSequence let y be set ; ::_thesis: ( y in rng (F ^ G) implies y is FinSequence ) assume y in rng (F ^ G) ; ::_thesis: y is FinSequence then ( y in rng F or y in rng G ) by A1, XBOOLE_0:def_3; hence y is FinSequence by Th26; ::_thesis: verum end; hence F ^ G is FinSequence-yielding by Th26; ::_thesis: verum end; end; registration let D be set ; let F be empty FinSequence of D * ; cluster FlattenSeq F -> empty ; coherence FlattenSeq F is empty proof F = <*> (D *) ; then FlattenSeq F = <*> D by Th2; hence FlattenSeq F is empty ; ::_thesis: verum end; end; theorem Th27: :: PRE_POLY:27 for D being set for F being FinSequence of D * holds len (FlattenSeq F) = Sum (Card F) proof let D be set ; ::_thesis: for F being FinSequence of D * holds len (FlattenSeq F) = Sum (Card F) defpred S1[ FinSequence of D * ] means len (FlattenSeq $1) = Sum (Card $1); A1: now__::_thesis:_for_F_being_FinSequence_of_D_*_ for_p_being_Element_of_D_*_st_S1[F]_holds_ S1[F_^_<*p*>] let F be FinSequence of D * ; ::_thesis: for p being Element of D * st S1[F] holds S1[F ^ <*p*>] let p be Element of D * ; ::_thesis: ( S1[F] implies S1[F ^ <*p*>] ) assume A2: S1[F] ; ::_thesis: S1[F ^ <*p*>] len (FlattenSeq (F ^ <*p*>)) = len ((FlattenSeq F) ^ (FlattenSeq <*p*>)) by Th3 .= (Sum (Card F)) + (len (FlattenSeq <*p*>)) by A2, FINSEQ_1:22 .= (Sum (Card F)) + (len p) by Th1 .= Sum ((Card F) ^ <*(len p)*>) by RVSUM_1:74 .= Sum ((Card F) ^ (Card <*p*>)) by Th24 .= Sum (Card (F ^ <*p*>)) by Th25 ; hence S1[F ^ <*p*>] ; ::_thesis: verum end; A3: S1[ <*> (D *)] by RVSUM_1:72; thus for F being FinSequence of D * holds S1[F] from FINSEQ_2:sch_2(A3, A1); ::_thesis: verum end; theorem Th28: :: PRE_POLY:28 for D, E being set for F being FinSequence of D * for G being FinSequence of E * st Card F = Card G holds len (FlattenSeq F) = len (FlattenSeq G) proof let D, E be set ; ::_thesis: for F being FinSequence of D * for G being FinSequence of E * st Card F = Card G holds len (FlattenSeq F) = len (FlattenSeq G) let F be FinSequence of D * ; ::_thesis: for G being FinSequence of E * st Card F = Card G holds len (FlattenSeq F) = len (FlattenSeq G) let G be FinSequence of E * ; ::_thesis: ( Card F = Card G implies len (FlattenSeq F) = len (FlattenSeq G) ) assume Card F = Card G ; ::_thesis: len (FlattenSeq F) = len (FlattenSeq G) hence len (FlattenSeq F) = Sum (Card G) by Th27 .= len (FlattenSeq G) by Th27 ; ::_thesis: verum end; theorem Th29: :: PRE_POLY:29 for D being set for F being FinSequence of D * for k being set st k in dom (FlattenSeq F) holds ex i, j being Element of NAT st ( i in dom F & j in dom (F . i) & k = (Sum (Card (F | (i -' 1)))) + j & (F . i) . j = (FlattenSeq F) . k ) proof let D be set ; ::_thesis: for F being FinSequence of D * for k being set st k in dom (FlattenSeq F) holds ex i, j being Element of NAT st ( i in dom F & j in dom (F . i) & k = (Sum (Card (F | (i -' 1)))) + j & (F . i) . j = (FlattenSeq F) . k ) set F = <*> (D *); defpred S1[ FinSequence of D * ] means for k being set st k in dom (FlattenSeq $1) holds ex i, j being Element of NAT st ( i in dom $1 & j in dom ($1 . i) & k = (Sum (Card ($1 | (i -' 1)))) + j & ($1 . i) . j = (FlattenSeq $1) . k ); A1: for F being FinSequence of D * for p being Element of D * st S1[F] holds S1[F ^ <*p*>] proof let F be FinSequence of D * ; ::_thesis: for p being Element of D * st S1[F] holds S1[F ^ <*p*>] let p be Element of D * ; ::_thesis: ( S1[F] implies S1[F ^ <*p*>] ) assume A2: S1[F] ; ::_thesis: S1[F ^ <*p*>] let k be set ; ::_thesis: ( k in dom (FlattenSeq (F ^ <*p*>)) implies ex i, j being Element of NAT st ( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) ) A3: FlattenSeq (F ^ <*p*>) = (FlattenSeq F) ^ (FlattenSeq <*p*>) by Th3 .= (FlattenSeq F) ^ p by Th1 ; A4: ( Sum (Card F) = len (FlattenSeq F) & (F ^ <*p*>) | (len F) = F ) by Th27, FINSEQ_5:23; assume A5: k in dom (FlattenSeq (F ^ <*p*>)) ; ::_thesis: ex i, j being Element of NAT st ( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) then reconsider m = k as Element of NAT ; percases ( not k in dom (FlattenSeq F) or k in dom (FlattenSeq F) ) ; supposeA6: not k in dom (FlattenSeq F) ; ::_thesis: ex i, j being Element of NAT st ( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) take i = (len F) + 1; ::_thesis: ex j being Element of NAT st ( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) take j = m -' (Sum (Card ((F ^ <*p*>) | (i -' 1)))); ::_thesis: ( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) A7: 1 <= (len F) + 1 by NAT_1:11; len (F ^ <*p*>) = (len F) + (len <*p*>) by FINSEQ_1:22 .= (len F) + 1 by FINSEQ_1:39 ; hence i in dom (F ^ <*p*>) by A7, FINSEQ_3:25; ::_thesis: ( j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) A8: Sum (Card ((F ^ <*p*>) | (i -' 1))) = len (FlattenSeq F) by A4, NAT_D:34; m <= len ((FlattenSeq F) ^ p) by A5, A3, FINSEQ_3:25; then m <= (len (FlattenSeq F)) + (len p) by FINSEQ_1:22; then A9: j <= len p by A8, NAT_D:53; 1 in dom <*p*> by FINSEQ_5:6; then A10: (F ^ <*p*>) . i = <*p*> . 1 by FINSEQ_1:def_7 .= p by FINSEQ_1:40 ; 1 <= m by A5, FINSEQ_3:25; then A11: len (FlattenSeq F) < m by A6, FINSEQ_3:25; then (len (FlattenSeq F)) + 1 <= m by NAT_1:13; then 1 <= j by A8, NAT_D:55; hence A12: j in dom ((F ^ <*p*>) . i) by A10, A9, FINSEQ_3:25; ::_thesis: ( k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) thus k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j by A8, A11, XREAL_1:235; ::_thesis: ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k hence ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k by A3, A8, A10, A12, FINSEQ_1:def_7; ::_thesis: verum end; supposeA13: k in dom (FlattenSeq F) ; ::_thesis: ex i, j being Element of NAT st ( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) then consider i, j being Element of NAT such that A14: i in dom F and A15: j in dom (F . i) and A16: k = (Sum (Card (F | (i -' 1)))) + j and A17: (F . i) . j = (FlattenSeq F) . k by A2; take i ; ::_thesis: ex j being Element of NAT st ( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) take j ; ::_thesis: ( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) dom F c= dom (F ^ <*p*>) by FINSEQ_1:26; hence i in dom (F ^ <*p*>) by A14; ::_thesis: ( j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) thus j in dom ((F ^ <*p*>) . i) by A14, A15, FINSEQ_1:def_7; ::_thesis: ( k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) A18: i -' 1 <= i by NAT_D:35; i <= len F by A14, FINSEQ_3:25; hence k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j by A16, A18, FINSEQ_5:22, XXREAL_0:2; ::_thesis: ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k (F ^ <*p*>) . i = F . i by A14, FINSEQ_1:def_7; hence ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k by A3, A13, A17, FINSEQ_1:def_7; ::_thesis: verum end; end; end; A19: S1[ <*> (D *)] ; thus for F being FinSequence of D * holds S1[F] from FINSEQ_2:sch_2(A19, A1); ::_thesis: verum end; theorem Th30: :: PRE_POLY:30 for D being set for F being FinSequence of D * for i, j being Element of NAT st i in dom F & j in dom (F . i) holds ( (Sum (Card (F | (i -' 1)))) + j in dom (FlattenSeq F) & (F . i) . j = (FlattenSeq F) . ((Sum (Card (F | (i -' 1)))) + j) ) proof let D be set ; ::_thesis: for F being FinSequence of D * for i, j being Element of NAT st i in dom F & j in dom (F . i) holds ( (Sum (Card (F | (i -' 1)))) + j in dom (FlattenSeq F) & (F . i) . j = (FlattenSeq F) . ((Sum (Card (F | (i -' 1)))) + j) ) set F = <*> (D *); defpred S1[ FinSequence of D * ] means for i, j being Element of NAT st i in dom $1 & j in dom ($1 . i) holds ( (Sum (Card ($1 | (i -' 1)))) + j in dom (FlattenSeq $1) & ($1 . i) . j = (FlattenSeq $1) . ((Sum (Card ($1 | (i -' 1)))) + j) ); A1: for F being FinSequence of D * for p being Element of D * st S1[F] holds S1[F ^ <*p*>] proof let F be FinSequence of D * ; ::_thesis: for p being Element of D * st S1[F] holds S1[F ^ <*p*>] let p be Element of D * ; ::_thesis: ( S1[F] implies S1[F ^ <*p*>] ) assume A2: for i, j being Element of NAT st i in dom F & j in dom (F . i) holds ( (Sum (Card (F | (i -' 1)))) + j in dom (FlattenSeq F) & (F . i) . j = (FlattenSeq F) . ((Sum (Card (F | (i -' 1)))) + j) ) ; ::_thesis: S1[F ^ <*p*>] let i, j be Element of NAT ; ::_thesis: ( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) implies ( (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>)) & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) ) ) assume that A3: i in dom (F ^ <*p*>) and A4: j in dom ((F ^ <*p*>) . i) ; ::_thesis: ( (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>)) & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) ) A5: FlattenSeq (F ^ <*p*>) = (FlattenSeq F) ^ (FlattenSeq <*p*>) by Th3 .= (FlattenSeq F) ^ p by Th1 ; percases ( not i in dom F or i in dom F ) ; supposeA6: not i in dom F ; ::_thesis: ( (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>)) & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) ) 1 <= i by A3, FINSEQ_3:25; then len F < i by A6, FINSEQ_3:25; then A7: (len F) + 1 <= i by NAT_1:13; A8: len (F ^ <*p*>) = (len F) + (len <*p*>) by FINSEQ_1:22 .= (len F) + 1 by FINSEQ_1:40 ; i <= len (F ^ <*p*>) by A3, FINSEQ_3:25; then A9: i = (len F) + 1 by A8, A7, XXREAL_0:1; then i -' 1 = len F by NAT_D:34; then A10: (F ^ <*p*>) | (i -' 1) = F by FINSEQ_5:23; A11: Sum (Card F) = len (FlattenSeq F) by Th27; 1 in dom <*p*> by FINSEQ_5:6; then A12: (F ^ <*p*>) . i = <*p*> . 1 by A9, FINSEQ_1:def_7 .= p by FINSEQ_1:40 ; hence (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>)) by A4, A5, A10, A11, FINSEQ_1:28; ::_thesis: ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) thus ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) by A4, A5, A12, A10, A11, FINSEQ_1:def_7; ::_thesis: verum end; supposeA13: i in dom F ; ::_thesis: ( (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>)) & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) ) then A14: j in dom (F . i) by A4, FINSEQ_1:def_7; then A15: (Sum (Card (F | (i -' 1)))) + j in dom (FlattenSeq F) by A2, A13; A16: i -' 1 <= i by NAT_D:35; i <= len F by A13, FINSEQ_3:25; then A17: (F ^ <*p*>) | (i -' 1) = F | (i -' 1) by A16, FINSEQ_5:22, XXREAL_0:2; dom (FlattenSeq F) c= dom (FlattenSeq (F ^ <*p*>)) by A5, FINSEQ_1:26; hence (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>)) by A17, A15; ::_thesis: ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) thus ((F ^ <*p*>) . i) . j = (F . i) . j by A13, FINSEQ_1:def_7 .= (FlattenSeq F) . ((Sum (Card (F | (i -' 1)))) + j) by A2, A13, A14 .= (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) by A5, A17, A15, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; A18: S1[ <*> (D *)] ; thus for F being FinSequence of D * holds S1[F] from FINSEQ_2:sch_2(A18, A1); ::_thesis: verum end; theorem Th31: :: PRE_POLY:31 for X, Y being non empty set for f being FinSequence of X * for v being Function of X,Y holds ((dom f) --> v) ** f is FinSequence of Y * proof let X, Y be non empty set ; ::_thesis: for f being FinSequence of X * for v being Function of X,Y holds ((dom f) --> v) ** f is FinSequence of Y * let f be FinSequence of X * ; ::_thesis: for v being Function of X,Y holds ((dom f) --> v) ** f is FinSequence of Y * let v be Function of X,Y; ::_thesis: ((dom f) --> v) ** f is FinSequence of Y * set F = ((dom f) --> v) ** f; A1: dom (((dom f) --> v) ** f) = (dom ((dom f) --> v)) /\ (dom f) by PBOOLE:def_19 .= (dom f) /\ (dom f) by FUNCOP_1:13 .= dom f ; A2: rng (((dom f) --> v) ** f) c= Y * proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (((dom f) --> v) ** f) or y in Y * ) assume y in rng (((dom f) --> v) ** f) ; ::_thesis: y in Y * then consider x being set such that A3: x in dom (((dom f) --> v) ** f) and A4: y = (((dom f) --> v) ** f) . x by FUNCT_1:def_3; reconsider x = x as Element of NAT by A1, A3; f . x in X * by A1, A3, FINSEQ_2:11; then A5: f . x is FinSequence of X by FINSEQ_1:def_11; y = (((dom f) --> v) . x) * (f . x) by A3, A4, PBOOLE:def_19 .= v * (f . x) by A1, A3, FUNCOP_1:7 ; then y is FinSequence of Y by A5, FINSEQ_2:32; hence y in Y * by FINSEQ_1:def_11; ::_thesis: verum end; dom (((dom f) --> v) ** f) = Seg (len f) by A1, FINSEQ_1:def_3; then ((dom f) --> v) ** f is FinSequence-like by FINSEQ_1:def_2; hence ((dom f) --> v) ** f is FinSequence of Y * by A2, FINSEQ_1:def_4; ::_thesis: verum end; theorem :: PRE_POLY:32 for X, Y being non empty set for f being FinSequence of X * for v being Function of X,Y ex F being FinSequence of Y * st ( F = ((dom f) --> v) ** f & v * (FlattenSeq f) = FlattenSeq F ) proof let X, Y be non empty set ; ::_thesis: for f being FinSequence of X * for v being Function of X,Y ex F being FinSequence of Y * st ( F = ((dom f) --> v) ** f & v * (FlattenSeq f) = FlattenSeq F ) let f be FinSequence of X * ; ::_thesis: for v being Function of X,Y ex F being FinSequence of Y * st ( F = ((dom f) --> v) ** f & v * (FlattenSeq f) = FlattenSeq F ) let v be Function of X,Y; ::_thesis: ex F being FinSequence of Y * st ( F = ((dom f) --> v) ** f & v * (FlattenSeq f) = FlattenSeq F ) reconsider F = ((dom f) --> v) ** f as FinSequence of Y * by Th31; take F ; ::_thesis: ( F = ((dom f) --> v) ** f & v * (FlattenSeq f) = FlattenSeq F ) thus F = ((dom f) --> v) ** f ; ::_thesis: v * (FlattenSeq f) = FlattenSeq F set Fl = FlattenSeq F; set fl = FlattenSeq f; reconsider vfl = v * (FlattenSeq f) as FinSequence of Y ; now__::_thesis:_(_dom_(FlattenSeq_f)_=_dom_vfl_&_dom_(FlattenSeq_f)_=_dom_(FlattenSeq_F)_&_(_for_k_being_Nat_st_k_in_dom_(FlattenSeq_f)_holds_ vfl_._k_=_(FlattenSeq_F)_._k_)_) len (FlattenSeq f) = len vfl by FINSEQ_2:33; hence A1: dom (FlattenSeq f) = dom vfl by FINSEQ_3:29; ::_thesis: ( dom (FlattenSeq f) = dom (FlattenSeq F) & ( for k being Nat st k in dom (FlattenSeq f) holds vfl . k = (FlattenSeq F) . k ) ) A2: dom F = (dom ((dom f) --> v)) /\ (dom f) by PBOOLE:def_19 .= (dom f) /\ (dom f) by FUNCOP_1:13 .= dom f ; A3: now__::_thesis:_for_k_being_set_st_k_in_dom_f_holds_ (Card_f)_._k_=_(Card_F)_._k let k be set ; ::_thesis: ( k in dom f implies (Card f) . k = (Card F) . k ) assume A4: k in dom f ; ::_thesis: (Card f) . k = (Card F) . k then reconsider k1 = k as Element of NAT ; A5: F . k = (((dom f) --> v) . k) * (f . k) by A2, A4, PBOOLE:def_19 .= v * (f . k) by A4, FUNCOP_1:7 ; f . k1 in X * by A4, FINSEQ_2:11; then reconsider fk = f . k as FinSequence of X by FINSEQ_1:def_11; thus (Card f) . k = len fk by A4, CARD_3:def_2 .= len (F . k) by A5, FINSEQ_2:33 .= (Card F) . k by A2, A4, CARD_3:def_2 ; ::_thesis: verum end; A6: ( dom f = dom (Card f) & dom f = dom (Card F) ) by A2, CARD_3:def_2; then A7: Card f = Card F by A3, FUNCT_1:2; len (FlattenSeq f) = len (FlattenSeq F) by A6, A3, Th28, FUNCT_1:2; hence dom (FlattenSeq f) = dom (FlattenSeq F) by FINSEQ_3:29; ::_thesis: for k being Nat st k in dom (FlattenSeq f) holds vfl . k = (FlattenSeq F) . k let k be Nat; ::_thesis: ( k in dom (FlattenSeq f) implies vfl . k = (FlattenSeq F) . k ) assume A8: k in dom (FlattenSeq f) ; ::_thesis: vfl . k = (FlattenSeq F) . k then consider i, j being Element of NAT such that A9: i in dom f and A10: j in dom (f . i) and A11: k = (Sum (Card (f | (i -' 1)))) + j and A12: (f . i) . j = (FlattenSeq f) . k by Th29; f . i in X * by A9, FINSEQ_2:11; then reconsider fi = f . i as FinSequence of X by FINSEQ_1:def_11; F . i = (((dom f) --> v) . i) * (f . i) by A2, A9, PBOOLE:def_19 .= v * (f . i) by A9, FUNCOP_1:7 ; then len fi = len (F . i) by FINSEQ_2:33; then A13: j in dom (F . i) by A10, FINSEQ_3:29; f . i in X * by A9, FINSEQ_2:11; then ( dom v = X & f . i is FinSequence of X ) by FINSEQ_1:def_11, FUNCT_2:def_1; then rng (f . i) c= dom v by FINSEQ_1:def_4; then A14: j in dom (v * (f . i)) by A10, RELAT_1:27; Card (F | (i -' 1)) = Card (F | (Seg (i -' 1))) by FINSEQ_1:def_15 .= (Card f) | (Seg (i -' 1)) by A7, Th23 .= Card (f | (Seg (i -' 1))) by Th23 .= Card (f | (i -' 1)) by FINSEQ_1:def_15 ; then (FlattenSeq F) . k = (F . i) . j by A2, A9, A11, A13, Th30 .= ((((dom f) --> v) . i) * (f . i)) . j by A2, A9, PBOOLE:def_19 .= (v * (f . i)) . j by A9, FUNCOP_1:7 .= v . ((f . i) . j) by A14, FUNCT_1:12 ; hence vfl . k = (FlattenSeq F) . k by A1, A8, A12, FUNCT_1:12; ::_thesis: verum end; hence v * (FlattenSeq f) = FlattenSeq F by FINSEQ_1:13; ::_thesis: verum end; begin registration let f be natural-valued Function; let x be set ; let n be Nat; clusterf +* (x,n) -> natural-valued ; coherence f +* (x,n) is natural-valued proof set F = f +* (x,n); let a be set ; :: according to VALUED_0:def_12 ::_thesis: ( not a in dom (f +* (x,n)) or (f +* (x,n)) . a is natural ) assume a in dom (f +* (x,n)) ; ::_thesis: (f +* (x,n)) . a is natural percases ( ( x in dom f & x = a ) or ( x in dom f & x <> a ) or not x in dom f ) ; suppose ( x in dom f & x = a ) ; ::_thesis: (f +* (x,n)) . a is natural hence (f +* (x,n)) . a is natural by FUNCT_7:31; ::_thesis: verum end; suppose ( x in dom f & x <> a ) ; ::_thesis: (f +* (x,n)) . a is natural then (f +* (x,n)) . a = f . a by FUNCT_7:32; hence (f +* (x,n)) . a is natural ; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: (f +* (x,n)) . a is natural then (f +* (x,n)) . a = f . a by FUNCT_7:def_3; hence (f +* (x,n)) . a is natural ; ::_thesis: verum end; end; end; end; registration let f be real-valued Function; let x be set ; let n be real number ; clusterf +* (x,n) -> real-valued ; coherence f +* (x,n) is real-valued proof set F = f +* (x,n); let a be set ; :: according to VALUED_0:def_9 ::_thesis: ( not a in dom (f +* (x,n)) or (f +* (x,n)) . a is real ) assume a in dom (f +* (x,n)) ; ::_thesis: (f +* (x,n)) . a is real percases ( ( x in dom f & x = a ) or ( x in dom f & x <> a ) or not x in dom f ) ; suppose ( x in dom f & x = a ) ; ::_thesis: (f +* (x,n)) . a is real hence (f +* (x,n)) . a is real by FUNCT_7:31; ::_thesis: verum end; suppose ( x in dom f & x <> a ) ; ::_thesis: (f +* (x,n)) . a is real then (f +* (x,n)) . a = f . a by FUNCT_7:32; hence (f +* (x,n)) . a is real ; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: (f +* (x,n)) . a is real then (f +* (x,n)) . a = f . a by FUNCT_7:def_3; hence (f +* (x,n)) . a is real ; ::_thesis: verum end; end; end; end; definition let X be set ; let b1, b2 be complex-valued ManySortedSet of X; :: original: + redefine funcb1 + b2 -> ManySortedSet of X means :Def5: :: PRE_POLY:def 5 for x being set holds it . x = (b1 . x) + (b2 . x); coherence b1 + b2 is ManySortedSet of X ; compatibility for b1 being ManySortedSet of X holds ( b1 = b1 + b2 iff for x being set holds b1 . x = (b1 . x) + (b2 . x) ) proof let f be ManySortedSet of X; ::_thesis: ( f = b1 + b2 iff for x being set holds f . x = (b1 . x) + (b2 . x) ) A1: ( dom b1 = X & dom b2 = X ) by PARTFUN1:def_2; then A2: dom f = (dom b1) /\ (dom b2) by PARTFUN1:def_2; thus ( f = b1 + b2 implies for x being set holds f . x = (b1 . x) + (b2 . x) ) ::_thesis: ( ( for x being set holds f . x = (b1 . x) + (b2 . x) ) implies f = b1 + b2 ) proof assume A3: f = b1 + b2 ; ::_thesis: for x being set holds f . x = (b1 . x) + (b2 . x) let x be set ; ::_thesis: f . x = (b1 . x) + (b2 . x) percases ( x in X or not x in X ) ; suppose x in X ; ::_thesis: f . x = (b1 . x) + (b2 . x) hence f . x = (b1 . x) + (b2 . x) by A1, A2, A3, VALUED_1:def_1; ::_thesis: verum end; supposeA4: not x in X ; ::_thesis: f . x = (b1 . x) + (b2 . x) then ( b1 . x = 0 & b2 . x = 0 ) by A1, FUNCT_1:def_2; hence f . x = (b1 . x) + (b2 . x) by A1, A2, A4, FUNCT_1:def_2; ::_thesis: verum end; end; end; assume for x being set holds f . x = (b1 . x) + (b2 . x) ; ::_thesis: f = b1 + b2 then for c being set st c in dom f holds f . c = (b1 . c) + (b2 . c) ; hence f = b1 + b2 by A2, VALUED_1:def_1; ::_thesis: verum end; end; :: deftheorem Def5 defines + PRE_POLY:def_5_:_ for X being set for b1, b2 being complex-valued ManySortedSet of X for b4 being ManySortedSet of X holds ( b4 = b1 + b2 iff for x being set holds b4 . x = (b1 . x) + (b2 . x) ); definition let X be set ; let b1, b2 be natural-valued ManySortedSet of X; funcb1 -' b2 -> ManySortedSet of X means :Def6: :: PRE_POLY:def 6 for x being set holds it . x = (b1 . x) -' (b2 . x); existence ex b1 being ManySortedSet of X st for x being set holds b1 . x = (b1 . x) -' (b2 . x) proof deffunc H1( set ) -> Element of NAT = (b1 . $1) -' (b2 . $1); consider f being ManySortedSet of X such that A1: for i being set st i in X holds f . i = H1(i) from PBOOLE:sch_4(); take f ; ::_thesis: for x being set holds f . x = (b1 . x) -' (b2 . x) let x be set ; ::_thesis: f . x = (b1 . x) -' (b2 . x) percases ( x in X or not x in X ) ; suppose x in X ; ::_thesis: f . x = (b1 . x) -' (b2 . x) hence f . x = (b1 . x) -' (b2 . x) by A1; ::_thesis: verum end; supposeA2: not x in X ; ::_thesis: f . x = (b1 . x) -' (b2 . x) A3: dom b2 = X by PARTFUN1:def_2; A4: dom b1 = X by PARTFUN1:def_2; dom f = X by PARTFUN1:def_2; hence f . x = 0 by A2, FUNCT_1:def_2 .= 0 -' 0 by XREAL_1:232 .= 0 -' (b2 . x) by A2, A3, FUNCT_1:def_2 .= (b1 . x) -' (b2 . x) by A2, A4, FUNCT_1:def_2 ; ::_thesis: verum end; end; end; uniqueness for b1, b2 being ManySortedSet of X st ( for x being set holds b1 . x = (b1 . x) -' (b2 . x) ) & ( for x being set holds b2 . x = (b1 . x) -' (b2 . x) ) holds b1 = b2 proof let it1, it2 be ManySortedSet of X; ::_thesis: ( ( for x being set holds it1 . x = (b1 . x) -' (b2 . x) ) & ( for x being set holds it2 . x = (b1 . x) -' (b2 . x) ) implies it1 = it2 ) assume that A5: for x being set holds it1 . x = (b1 . x) -' (b2 . x) and A6: for x being set holds it2 . x = (b1 . x) -' (b2 . x) ; ::_thesis: it1 = it2 now__::_thesis:_for_x_being_set_st_x_in_X_holds_ it1_._x_=_it2_._x let x be set ; ::_thesis: ( x in X implies it1 . x = it2 . x ) assume x in X ; ::_thesis: it1 . x = it2 . x thus it1 . x = (b1 . x) -' (b2 . x) by A5 .= it2 . x by A6 ; ::_thesis: verum end; hence it1 = it2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def6 defines -' PRE_POLY:def_6_:_ for X being set for b1, b2 being natural-valued ManySortedSet of X for b4 being ManySortedSet of X holds ( b4 = b1 -' b2 iff for x being set holds b4 . x = (b1 . x) -' (b2 . x) ); theorem :: PRE_POLY:33 for X being set for b, b1, b2 being real-valued ManySortedSet of X st ( for x being set st x in X holds b . x = (b1 . x) + (b2 . x) ) holds b = b1 + b2 proof let X be set ; ::_thesis: for b, b1, b2 being real-valued ManySortedSet of X st ( for x being set st x in X holds b . x = (b1 . x) + (b2 . x) ) holds b = b1 + b2 let b, b1, b2 be real-valued ManySortedSet of X; ::_thesis: ( ( for x being set st x in X holds b . x = (b1 . x) + (b2 . x) ) implies b = b1 + b2 ) assume A1: for x being set st x in X holds b . x = (b1 . x) + (b2 . x) ; ::_thesis: b = b1 + b2 now__::_thesis:_for_x_being_set_holds_b_._x_=_(b1_._x)_+_(b2_._x) let x be set ; ::_thesis: b . b1 = (b1 . b1) + (b2 . b1) percases ( x in X or not x in X ) ; suppose x in X ; ::_thesis: b . b1 = (b1 . b1) + (b2 . b1) hence b . x = (b1 . x) + (b2 . x) by A1; ::_thesis: verum end; supposeA2: not x in X ; ::_thesis: b . b1 = (b1 . b1) + (b2 . b1) A3: dom b2 = X by PARTFUN1:def_2; A4: dom b1 = X by PARTFUN1:def_2; dom b = X by PARTFUN1:def_2; hence b . x = 0 + 0 by A2, FUNCT_1:def_2 .= 0 + (b2 . x) by A2, A3, FUNCT_1:def_2 .= (b1 . x) + (b2 . x) by A2, A4, FUNCT_1:def_2 ; ::_thesis: verum end; end; end; hence b = b1 + b2 by Def5; ::_thesis: verum end; theorem Th34: :: PRE_POLY:34 for X being set for b, b1, b2 being natural-valued ManySortedSet of X st ( for x being set st x in X holds b . x = (b1 . x) -' (b2 . x) ) holds b = b1 -' b2 proof let X be set ; ::_thesis: for b, b1, b2 being natural-valued ManySortedSet of X st ( for x being set st x in X holds b . x = (b1 . x) -' (b2 . x) ) holds b = b1 -' b2 let b, b1, b2 be natural-valued ManySortedSet of X; ::_thesis: ( ( for x being set st x in X holds b . x = (b1 . x) -' (b2 . x) ) implies b = b1 -' b2 ) assume A1: for x being set st x in X holds b . x = (b1 . x) -' (b2 . x) ; ::_thesis: b = b1 -' b2 now__::_thesis:_for_x_being_set_holds_b_._x_=_(b1_._x)_-'_(b2_._x) let x be set ; ::_thesis: b . b1 = (b1 . b1) -' (b2 . b1) percases ( x in X or not x in X ) ; suppose x in X ; ::_thesis: b . b1 = (b1 . b1) -' (b2 . b1) hence b . x = (b1 . x) -' (b2 . x) by A1; ::_thesis: verum end; supposeA2: not x in X ; ::_thesis: b . b1 = (b1 . b1) -' (b2 . b1) A3: dom b2 = X by PARTFUN1:def_2; A4: dom b1 = X by PARTFUN1:def_2; dom b = X by PARTFUN1:def_2; hence b . x = 0 by A2, FUNCT_1:def_2 .= 0 -' 0 by XREAL_1:232 .= 0 -' (b2 . x) by A2, A3, FUNCT_1:def_2 .= (b1 . x) -' (b2 . x) by A2, A4, FUNCT_1:def_2 ; ::_thesis: verum end; end; end; hence b = b1 -' b2 by Def6; ::_thesis: verum end; registration let X be set ; let b1, b2 be natural-valued ManySortedSet of X; clusterb1 + b2 -> natural-valued ; coherence b1 + b2 is natural-valued ; clusterb1 -' b2 -> natural-valued ; coherence b1 -' b2 is natural-valued proof set f = b1 -' b2; rng (b1 -' b2) c= NAT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (b1 -' b2) or y in NAT ) assume y in rng (b1 -' b2) ; ::_thesis: y in NAT then consider x being set such that x in dom (b1 -' b2) and A1: y = (b1 -' b2) . x by FUNCT_1:def_3; (b1 -' b2) . x = (b1 . x) -' (b2 . x) by Def6; hence y in NAT by A1; ::_thesis: verum end; hence b1 -' b2 is natural-valued by VALUED_0:def_6; ::_thesis: verum end; end; theorem Th35: :: PRE_POLY:35 for X being set for b1, b2, b3 being real-valued ManySortedSet of X holds (b1 + b2) + b3 = b1 + (b2 + b3) proof let X be set ; ::_thesis: for b1, b2, b3 being real-valued ManySortedSet of X holds (b1 + b2) + b3 = b1 + (b2 + b3) let b1, b2, b3 be real-valued ManySortedSet of X; ::_thesis: (b1 + b2) + b3 = b1 + (b2 + b3) now__::_thesis:_for_x_being_set_st_x_in_X_holds_ ((b1_+_b2)_+_b3)_._x_=_(b1_+_(b2_+_b3))_._x let x be set ; ::_thesis: ( x in X implies ((b1 + b2) + b3) . x = (b1 + (b2 + b3)) . x ) assume x in X ; ::_thesis: ((b1 + b2) + b3) . x = (b1 + (b2 + b3)) . x thus ((b1 + b2) + b3) . x = ((b1 + b2) . x) + (b3 . x) by Def5 .= ((b1 . x) + (b2 . x)) + (b3 . x) by Def5 .= (b1 . x) + ((b2 . x) + (b3 . x)) .= (b1 . x) + ((b2 + b3) . x) by Def5 .= (b1 + (b2 + b3)) . x by Def5 ; ::_thesis: verum end; hence (b1 + b2) + b3 = b1 + (b2 + b3) by PBOOLE:3; ::_thesis: verum end; theorem :: PRE_POLY:36 for X being set for b, c, d being natural-valued ManySortedSet of X holds (b -' c) -' d = b -' (c + d) proof let X be set ; ::_thesis: for b, c, d being natural-valued ManySortedSet of X holds (b -' c) -' d = b -' (c + d) let b, c, d be natural-valued ManySortedSet of X; ::_thesis: (b -' c) -' d = b -' (c + d) now__::_thesis:_for_x_being_set_st_x_in_X_holds_ ((b_-'_c)_-'_d)_._x_=_(b_._x)_-'_((c_+_d)_._x) let x be set ; ::_thesis: ( x in X implies ((b -' c) -' d) . x = (b . x) -' ((c + d) . x) ) assume x in X ; ::_thesis: ((b -' c) -' d) . x = (b . x) -' ((c + d) . x) thus ((b -' c) -' d) . x = ((b -' c) . x) -' (d . x) by Def6 .= ((b . x) -' (c . x)) -' (d . x) by Def6 .= (b . x) -' ((c . x) + (d . x)) by NAT_2:30 .= (b . x) -' ((c + d) . x) by Def5 ; ::_thesis: verum end; hence (b -' c) -' d = b -' (c + d) by Th34; ::_thesis: verum end; begin definition let f be Function; func support f -> set means :Def7: :: PRE_POLY:def 7 for x being set holds ( x in it iff f . x <> 0 ); existence ex b1 being set st for x being set holds ( x in b1 iff f . x <> 0 ) proof defpred S1[ set ] means f . $1 <> 0 ; consider A being set such that A1: for x being set holds ( x in A iff ( x in dom f & S1[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for x being set holds ( x in A iff f . x <> 0 ) let x be set ; ::_thesis: ( x in A iff f . x <> 0 ) thus ( x in A implies f . x <> 0 ) by A1; ::_thesis: ( f . x <> 0 implies x in A ) assume A2: f . x <> 0 ; ::_thesis: x in A then x in dom f by FUNCT_1:def_2; hence x in A by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff f . x <> 0 ) ) & ( for x being set holds ( x in b2 iff f . x <> 0 ) ) holds b1 = b2 proof let A, B be set ; ::_thesis: ( ( for x being set holds ( x in A iff f . x <> 0 ) ) & ( for x being set holds ( x in B iff f . x <> 0 ) ) implies A = B ) assume that A3: for x being set holds ( x in A iff f . x <> 0 ) and A4: for x being set holds ( x in B iff f . x <> 0 ) ; ::_thesis: A = B for x being set holds ( x in A iff x in B ) proof let x be set ; ::_thesis: ( x in A iff x in B ) ( x in A iff f . x <> 0 ) by A3; hence ( x in A iff x in B ) by A4; ::_thesis: verum end; hence A = B by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def7 defines support PRE_POLY:def_7_:_ for f being Function for b2 being set holds ( b2 = support f iff for x being set holds ( x in b2 iff f . x <> 0 ) ); theorem Th37: :: PRE_POLY:37 for f being Function holds support f c= dom f proof let f be Function; ::_thesis: support f c= dom f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support f or x in dom f ) assume x in support f ; ::_thesis: x in dom f then f . x <> 0 by Def7; hence x in dom f by FUNCT_1:def_2; ::_thesis: verum end; definition let f be Function; attrf is finite-support means :Def8: :: PRE_POLY:def 8 support f is finite ; end; :: deftheorem Def8 defines finite-support PRE_POLY:def_8_:_ for f being Function holds ( f is finite-support iff support f is finite ); registration cluster Relation-like Function-like finite -> finite-support for set ; coherence for b1 being Function st b1 is finite holds b1 is finite-support proof let f be Function; ::_thesis: ( f is finite implies f is finite-support ) assume f is finite ; ::_thesis: f is finite-support then dom f is finite ; hence support f is finite by Th37, FINSET_1:1; :: according to PRE_POLY:def_8 ::_thesis: verum end; end; registration cluster Relation-like Function-like non empty natural-valued finite-support for set ; existence ex b1 being Function st ( b1 is natural-valued & b1 is finite-support & not b1 is empty ) proof take f = 0 .--> 1; ::_thesis: ( f is natural-valued & f is finite-support & not f is empty ) thus f is natural-valued ; ::_thesis: ( f is finite-support & not f is empty ) thus f is finite-support ; ::_thesis: not f is empty thus not f is empty ; ::_thesis: verum end; end; registration let f be finite-support Function; cluster support f -> finite ; coherence support f is finite by Def8; end; registration let X be set ; cluster Relation-like X -defined NAT -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued finite-support for Element of bool [:X,NAT:]; existence ex b1 being Function of X,NAT st b1 is finite-support proof set f = X --> 0; A1: dom (X --> 0) = X by FUNCOP_1:13; reconsider f = X --> 0 as Function of X,NAT ; take f ; ::_thesis: f is finite-support now__::_thesis:_not_support_f_<>_{} A2: support f c= dom f by Th37; assume support f <> {} ; ::_thesis: contradiction then consider x being set such that A3: x in support f by XBOOLE_0:def_1; f . x <> 0 by A3, Def7; hence contradiction by A1, A3, A2, FUNCOP_1:7; ::_thesis: verum end; hence support f is finite ; :: according to PRE_POLY:def_8 ::_thesis: verum end; end; registration let f be finite-support Function; let x, y be set ; clusterf +* (x,y) -> finite-support ; coherence f +* (x,y) is finite-support proof set F = f +* (x,y); support (f +* (x,y)) c= (support f) \/ {x} proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in support (f +* (x,y)) or a in (support f) \/ {x} ) assume a in support (f +* (x,y)) ; ::_thesis: a in (support f) \/ {x} then A1: (f +* (x,y)) . a <> 0 by Def7; percases ( ( x in dom f & a = x ) or ( x in dom f & a <> x ) or not x in dom f ) ; suppose ( x in dom f & a = x ) ; ::_thesis: a in (support f) \/ {x} then a in {x} by TARSKI:def_1; hence a in (support f) \/ {x} by XBOOLE_0:def_3; ::_thesis: verum end; suppose ( x in dom f & a <> x ) ; ::_thesis: a in (support f) \/ {x} then (f +* (x,y)) . a = f . a by FUNCT_7:32; then a in support f by A1, Def7; hence a in (support f) \/ {x} by XBOOLE_0:def_3; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: a in (support f) \/ {x} then (f +* (x,y)) . a = f . a by FUNCT_7:def_3; then a in support f by A1, Def7; hence a in (support f) \/ {x} by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence support (f +* (x,y)) is finite ; :: according to PRE_POLY:def_8 ::_thesis: verum end; end; registration let X be set ; cluster Relation-like X -defined Function-like total natural-valued finite-support for set ; existence ex b1 being ManySortedSet of X st ( b1 is natural-valued & b1 is finite-support ) proof set f = X --> 0; A1: dom (X --> 0) = X by FUNCOP_1:13; reconsider f = X --> 0 as ManySortedSet of X ; take f ; ::_thesis: ( f is natural-valued & f is finite-support ) thus f is natural-valued ; ::_thesis: f is finite-support support f = {} proof assume not support f = {} ; ::_thesis: contradiction then consider x being set such that A2: x in support f by XBOOLE_0:def_1; support f c= dom f by Th37; then f . x = 0 by A1, A2, FUNCOP_1:7; hence contradiction by A2, Def7; ::_thesis: verum end; hence f is finite-support by Def8; ::_thesis: verum end; end; theorem Th38: :: PRE_POLY:38 for X being set for b1, b2 being natural-valued ManySortedSet of X holds support (b1 + b2) = (support b1) \/ (support b2) proof let X be set ; ::_thesis: for b1, b2 being natural-valued ManySortedSet of X holds support (b1 + b2) = (support b1) \/ (support b2) let b1, b2 be natural-valued ManySortedSet of X; ::_thesis: support (b1 + b2) = (support b1) \/ (support b2) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(support_b1)_\/_(support_b2)_implies_(b1_+_b2)_._x_<>_0_)_&_(_(b1_+_b2)_._x_<>_0_implies_x_in_(support_b1)_\/_(support_b2)_)_) let x be set ; ::_thesis: ( ( x in (support b1) \/ (support b2) implies (b1 + b2) . x <> 0 ) & ( (b1 + b2) . x <> 0 implies x in (support b1) \/ (support b2) ) ) hereby ::_thesis: ( (b1 + b2) . x <> 0 implies x in (support b1) \/ (support b2) ) assume x in (support b1) \/ (support b2) ; ::_thesis: (b1 + b2) . x <> 0 then ( x in support b1 or x in support b2 ) by XBOOLE_0:def_3; then ( b1 . x <> 0 or b2 . x <> 0 ) by Def7; then (b1 . x) + (b2 . x) <> 0 ; hence (b1 + b2) . x <> 0 by Def5; ::_thesis: verum end; assume A1: (b1 + b2) . x <> 0 ; ::_thesis: x in (support b1) \/ (support b2) assume A2: not x in (support b1) \/ (support b2) ; ::_thesis: contradiction then not x in support b1 by XBOOLE_0:def_3; then A3: b1 . x = 0 by Def7; not x in support b2 by A2, XBOOLE_0:def_3; then (b1 . x) + (b2 . x) = 0 by A3, Def7; hence contradiction by A1, Def5; ::_thesis: verum end; hence support (b1 + b2) = (support b1) \/ (support b2) by Def7; ::_thesis: verum end; theorem Th39: :: PRE_POLY:39 for X being set for b1, b2 being natural-valued ManySortedSet of X holds support (b1 -' b2) c= support b1 proof let X be set ; ::_thesis: for b1, b2 being natural-valued ManySortedSet of X holds support (b1 -' b2) c= support b1 let b1, b2 be natural-valued ManySortedSet of X; ::_thesis: support (b1 -' b2) c= support b1 thus support (b1 -' b2) c= support b1 ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (b1 -' b2) or x in support b1 ) assume A1: x in support (b1 -' b2) ; ::_thesis: x in support b1 assume not x in support b1 ; ::_thesis: contradiction then b1 . x = 0 by Def7; then (b1 . x) -' (b2 . x) = 0 by NAT_2:8; then (b1 -' b2) . x = 0 by Def6; hence contradiction by A1, Def7; ::_thesis: verum end; end; begin definition let X be set ; mode bag of X is natural-valued finite-support ManySortedSet of X; end; registration let X be finite set ; cluster Relation-like X -defined Function-like total -> finite-support for set ; coherence for b1 being ManySortedSet of X holds b1 is finite-support proof let f be ManySortedSet of X; ::_thesis: f is finite-support ( support f c= dom f & dom f = X ) by Th37, PARTFUN1:def_2; hence support f is finite ; :: according to PRE_POLY:def_8 ::_thesis: verum end; end; registration let X be set ; let b1, b2 be bag of X; clusterb1 + b2 -> finite-support ; coherence b1 + b2 is finite-support proof support (b1 + b2) = (support b1) \/ (support b2) by Th38; hence support (b1 + b2) is finite ; :: according to PRE_POLY:def_8 ::_thesis: verum end; clusterb1 -' b2 -> finite-support ; coherence b1 -' b2 is finite-support proof support (b1 -' b2) c= support b1 by Th39; hence support (b1 -' b2) is finite ; :: according to PRE_POLY:def_8 ::_thesis: verum end; end; theorem Th40: :: PRE_POLY:40 for X being set holds X --> 0 is bag of X proof let X be set ; ::_thesis: X --> 0 is bag of X set f = X --> 0; A1: dom (X --> 0) = X by FUNCOP_1:13; support (X --> 0) = {} proof assume not support (X --> 0) = {} ; ::_thesis: contradiction then consider x being set such that A2: x in support (X --> 0) by XBOOLE_0:def_1; support (X --> 0) c= dom (X --> 0) by Th37; then (X --> 0) . x = 0 by A1, A2, FUNCOP_1:7; hence contradiction by A2, Def7; ::_thesis: verum end; hence X --> 0 is bag of X by Def8; ::_thesis: verum end; definition let n be Ordinal; let p, q be bag of n; predp < q means :Def9: :: PRE_POLY:def 9 ex k being Ordinal st ( p . k < q . k & ( for l being Ordinal st l in k holds p . l = q . l ) ); asymmetry for p, q being bag of n st ex k being Ordinal st ( p . k < q . k & ( for l being Ordinal st l in k holds p . l = q . l ) ) holds for k being Ordinal holds ( not q . k < p . k or ex l being Ordinal st ( l in k & not q . l = p . l ) ) proof let p, q be bag of n; ::_thesis: ( ex k being Ordinal st ( p . k < q . k & ( for l being Ordinal st l in k holds p . l = q . l ) ) implies for k being Ordinal holds ( not q . k < p . k or ex l being Ordinal st ( l in k & not q . l = p . l ) ) ) given k being Ordinal such that A1: p . k < q . k and A2: for l being Ordinal st l in k holds p . l = q . l ; ::_thesis: for k being Ordinal holds ( not q . k < p . k or ex l being Ordinal st ( l in k & not q . l = p . l ) ) given k1 being Ordinal such that A3: q . k1 < p . k1 and A4: for l being Ordinal st l in k1 holds q . l = p . l ; ::_thesis: contradiction percases ( k in k1 or k1 in k or k1 = k ) by ORDINAL1:14; suppose k in k1 ; ::_thesis: contradiction hence contradiction by A1, A4; ::_thesis: verum end; suppose k1 in k ; ::_thesis: contradiction hence contradiction by A2, A3; ::_thesis: verum end; suppose k1 = k ; ::_thesis: contradiction hence contradiction by A1, A3; ::_thesis: verum end; end; end; end; :: deftheorem Def9 defines < PRE_POLY:def_9_:_ for n being Ordinal for p, q being bag of n holds ( p < q iff ex k being Ordinal st ( p . k < q . k & ( for l being Ordinal st l in k holds p . l = q . l ) ) ); theorem Th41: :: PRE_POLY:41 for n being Ordinal for p, q, r being bag of n st p < q & q < r holds p < r proof let n be Ordinal; ::_thesis: for p, q, r being bag of n st p < q & q < r holds p < r let p, q, r be bag of n; ::_thesis: ( p < q & q < r implies p < r ) assume that A1: p < q and A2: q < r ; ::_thesis: p < r consider k being Ordinal such that A3: p . k < q . k and A4: for l being Ordinal st l in k holds p . l = q . l by A1, Def9; consider m being Ordinal such that A5: q . m < r . m and A6: for l being Ordinal st l in m holds q . l = r . l by A2, Def9; take n = k /\ m; :: according to PRE_POLY:def_9 ::_thesis: ( p . n < r . n & ( for l being Ordinal st l in n holds p . l = r . l ) ) A7: ( ( n c= m & n <> m ) iff n c< m ) by XBOOLE_0:def_8; A8: ( ( n c= k & n <> k ) iff n c< k ) by XBOOLE_0:def_8; now__::_thesis:_p_._n_<_r_._n percases ( k in m or m in k or m = k ) by ORDINAL1:14; suppose k in m ; ::_thesis: p . n < r . n hence p . n < r . n by A3, A6, A8, A7, ORDINAL1:11, ORDINAL3:13, XBOOLE_1:17; ::_thesis: verum end; suppose m in k ; ::_thesis: p . n < r . n hence p . n < r . n by A4, A5, A8, A7, ORDINAL1:11, ORDINAL3:13, XBOOLE_1:17; ::_thesis: verum end; suppose m = k ; ::_thesis: p . n < r . n hence p . n < r . n by A3, A5, XXREAL_0:2; ::_thesis: verum end; end; end; hence p . n < r . n ; ::_thesis: for l being Ordinal st l in n holds p . l = r . l let l be Ordinal; ::_thesis: ( l in n implies p . l = r . l ) A9: n c= m by XBOOLE_1:17; assume A10: l in n ; ::_thesis: p . l = r . l n c= k by XBOOLE_1:17; hence p . l = q . l by A4, A10 .= r . l by A6, A9, A10 ; ::_thesis: verum end; definition let n be Ordinal; let p, q be bag of n; predp <=' q means :Def10: :: PRE_POLY:def 10 ( p < q or p = q ); reflexivity for p being bag of n holds ( p < p or p = p ) ; end; :: deftheorem Def10 defines <=' PRE_POLY:def_10_:_ for n being Ordinal for p, q being bag of n holds ( p <=' q iff ( p < q or p = q ) ); theorem Th42: :: PRE_POLY:42 for n being Ordinal for p, q, r being bag of n st p <=' q & q <=' r holds p <=' r proof let n be Ordinal; ::_thesis: for p, q, r being bag of n st p <=' q & q <=' r holds p <=' r let p, q, r be bag of n; ::_thesis: ( p <=' q & q <=' r implies p <=' r ) assume that A1: p <=' q and A2: q <=' r ; ::_thesis: p <=' r A3: ( q < r or q = r ) by A2, Def10; ( p < q or p = q ) by A1, Def10; then ( p < r or p <=' r ) by A3, Th41; hence p <=' r by Def10; ::_thesis: verum end; theorem :: PRE_POLY:43 for n being Ordinal for p, q, r being bag of n st p < q & q <=' r holds p < r proof let n be Ordinal; ::_thesis: for p, q, r being bag of n st p < q & q <=' r holds p < r let p, q, r be bag of n; ::_thesis: ( p < q & q <=' r implies p < r ) assume that A1: p < q and A2: q <=' r ; ::_thesis: p < r ( q < r or q = r ) by A2, Def10; hence p < r by A1, Th41; ::_thesis: verum end; theorem :: PRE_POLY:44 for n being Ordinal for p, q, r being bag of n st p <=' q & q < r holds p < r proof let n be Ordinal; ::_thesis: for p, q, r being bag of n st p <=' q & q < r holds p < r let p, q, r be bag of n; ::_thesis: ( p <=' q & q < r implies p < r ) assume that A1: p <=' q and A2: q < r ; ::_thesis: p < r ( p < q or p = q ) by A1, Def10; hence p < r by A2, Th41; ::_thesis: verum end; theorem Th45: :: PRE_POLY:45 for n being Ordinal for p, q being bag of n holds ( p <=' q or q <=' p ) proof let n be Ordinal; ::_thesis: for p, q being bag of n holds ( p <=' q or q <=' p ) let p, q be bag of n; ::_thesis: ( p <=' q or q <=' p ) assume A1: not p <=' q ; ::_thesis: q <=' p then consider i being set such that A2: i in n and A3: p . i <> q . i by PBOOLE:3; A4: not p < q by A1, Def10; defpred S1[ set ] means p . $1 <> q . $1; A5: ex i being Ordinal st S1[i] by A2, A3; consider m being Ordinal such that A6: S1[m] and A7: for n being Ordinal st S1[n] holds m c= n from ORDINAL1:sch_1(A5); A8: for l being Ordinal st l in m holds q . l = p . l by A7, ORDINAL1:5; percases ( p . m < q . m or p . m > q . m ) by A6, XXREAL_0:1; suppose p . m < q . m ; ::_thesis: q <=' p hence q <=' p by A4, A8, Def9; ::_thesis: verum end; suppose p . m > q . m ; ::_thesis: q <=' p then q < p by A8, Def9; hence q <=' p by Def10; ::_thesis: verum end; end; end; definition let X be set ; let d, b be bag of X; predd divides b means :Def11: :: PRE_POLY:def 11 for k being set holds d . k <= b . k; reflexivity for d being bag of X for k being set holds d . k <= d . k ; end; :: deftheorem Def11 defines divides PRE_POLY:def_11_:_ for X being set for d, b being bag of X holds ( d divides b iff for k being set holds d . k <= b . k ); theorem Th46: :: PRE_POLY:46 for n being set for d, b being bag of n st ( for k being set st k in n holds d . k <= b . k ) holds d divides b proof let n be set ; ::_thesis: for d, b being bag of n st ( for k being set st k in n holds d . k <= b . k ) holds d divides b let d, b be bag of n; ::_thesis: ( ( for k being set st k in n holds d . k <= b . k ) implies d divides b ) assume A1: for k being set st k in n holds d . k <= b . k ; ::_thesis: d divides b let k be set ; :: according to PRE_POLY:def_11 ::_thesis: d . k <= b . k percases ( k in dom d or not k in dom d ) ; suppose k in dom d ; ::_thesis: d . k <= b . k then k in n ; hence d . k <= b . k by A1; ::_thesis: verum end; suppose not k in dom d ; ::_thesis: d . k <= b . k hence d . k <= b . k by FUNCT_1:def_2; ::_thesis: verum end; end; end; theorem Th47: :: PRE_POLY:47 for n being Ordinal for b1, b2 being bag of n st b1 divides b2 holds (b2 -' b1) + b1 = b2 proof let n be Ordinal; ::_thesis: for b1, b2 being bag of n st b1 divides b2 holds (b2 -' b1) + b1 = b2 let b1, b2 be bag of n; ::_thesis: ( b1 divides b2 implies (b2 -' b1) + b1 = b2 ) assume A1: b1 divides b2 ; ::_thesis: (b2 -' b1) + b1 = b2 now__::_thesis:_for_k_being_set_st_k_in_n_holds_ ((b2_-'_b1)_+_b1)_._k_=_b2_._k let k be set ; ::_thesis: ( k in n implies ((b2 -' b1) + b1) . k = b2 . k ) assume k in n ; ::_thesis: ((b2 -' b1) + b1) . k = b2 . k then reconsider k9 = k as Ordinal ; A2: b1 . k9 <= b2 . k9 by A1, Def11; thus ((b2 -' b1) + b1) . k = ((b2 -' b1) . k) + (b1 . k) by Def5 .= ((b2 . k) -' (b1 . k)) + (b1 . k) by Def6 .= ((b2 . k) + (b1 . k)) -' (b1 . k) by A2, NAT_D:38 .= b2 . k by NAT_D:34 ; ::_thesis: verum end; hence (b2 -' b1) + b1 = b2 by PBOOLE:3; ::_thesis: verum end; theorem Th48: :: PRE_POLY:48 for X being set for b1, b2 being bag of X holds (b2 + b1) -' b1 = b2 proof let X be set ; ::_thesis: for b1, b2 being bag of X holds (b2 + b1) -' b1 = b2 let b1, b2 be bag of X; ::_thesis: (b2 + b1) -' b1 = b2 now__::_thesis:_for_k_being_set_st_k_in_X_holds_ ((b2_+_b1)_-'_b1)_._k_=_b2_._k let k be set ; ::_thesis: ( k in X implies ((b2 + b1) -' b1) . k = b2 . k ) assume k in X ; ::_thesis: ((b2 + b1) -' b1) . k = b2 . k thus ((b2 + b1) -' b1) . k = ((b2 + b1) . k) -' (b1 . k) by Def6 .= ((b2 . k) + (b1 . k)) -' (b1 . k) by Def5 .= b2 . k by NAT_D:34 ; ::_thesis: verum end; hence (b2 + b1) -' b1 = b2 by PBOOLE:3; ::_thesis: verum end; theorem Th49: :: PRE_POLY:49 for n being Ordinal for d, b being bag of n st d divides b holds d <=' b proof let n be Ordinal; ::_thesis: for d, b being bag of n st d divides b holds d <=' b let d, b be bag of n; ::_thesis: ( d divides b implies d <=' b ) assume that A1: d divides b and A2: not d < b ; :: according to PRE_POLY:def_10 ::_thesis: d = b now__::_thesis:_for_p_being_set_st_p_in_n_holds_ not_d_._p_<>_b_._p defpred S1[ set ] means d . $1 < b . $1; let p be set ; ::_thesis: ( p in n implies not d . p <> b . p ) assume p in n ; ::_thesis: not d . p <> b . p then reconsider p9 = p as Ordinal ; assume A3: d . p <> b . p ; ::_thesis: contradiction d . p9 <= b . p9 by A1, Def11; then d . p9 < b . p9 by A3, XXREAL_0:1; then A4: ex p being Ordinal st S1[p] ; consider k being Ordinal such that A5: S1[k] and A6: for m being Ordinal st S1[m] holds k c= m from ORDINAL1:sch_1(A4); now__::_thesis:_for_l_being_Ordinal_st_l_in_k_holds_ d_._l_=_b_._l let l be Ordinal; ::_thesis: ( l in k implies d . l = b . l ) assume l in k ; ::_thesis: d . l = b . l then A7: b . l <= d . l by A6, ORDINAL1:5; d . l <= b . l by A1, Def11; hence d . l = b . l by A7, XXREAL_0:1; ::_thesis: verum end; hence contradiction by A2, A5, Def9; ::_thesis: verum end; hence d = b by PBOOLE:3; ::_thesis: verum end; theorem Th50: :: PRE_POLY:50 for n being set for b, b1, b2 being bag of n st b = b1 + b2 holds b1 divides b proof let n be set ; ::_thesis: for b, b1, b2 being bag of n st b = b1 + b2 holds b1 divides b let b, b1, b2 be bag of n; ::_thesis: ( b = b1 + b2 implies b1 divides b ) assume A1: b = b1 + b2 ; ::_thesis: b1 divides b now__::_thesis:_for_k_being_set_st_k_in_n_holds_ b1_._k_<=_b_._k let k be set ; ::_thesis: ( k in n implies b1 . k <= b . k ) assume k in n ; ::_thesis: b1 . k <= b . k b . k = (b1 . k) + (b2 . k) by A1, Def5; hence b1 . k <= b . k by NAT_1:11; ::_thesis: verum end; hence b1 divides b by Th46; ::_thesis: verum end; definition let X be set ; func Bags X -> set means :Def12: :: PRE_POLY:def 12 for x being set holds ( x in it iff x is bag of X ); existence ex b1 being set st for x being set holds ( x in b1 iff x is bag of X ) proof defpred S1[ set ] means $1 is bag of X; consider A being set such that A1: for x being set holds ( x in A iff ( x in Funcs (X,NAT) & S1[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for x being set holds ( x in A iff x is bag of X ) let x be set ; ::_thesis: ( x in A iff x is bag of X ) thus ( x in A implies x is bag of X ) by A1; ::_thesis: ( x is bag of X implies x in A ) assume A2: x is bag of X ; ::_thesis: x in A then reconsider b = x as bag of X ; ( dom b = X & rng b c= NAT ) by PARTFUN1:def_2, VALUED_0:def_6; then x in Funcs (X,NAT) by FUNCT_2:def_2; hence x in A by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is bag of X ) ) & ( for x being set holds ( x in b2 iff x is bag of X ) ) holds b1 = b2 proof let A, B be set ; ::_thesis: ( ( for x being set holds ( x in A iff x is bag of X ) ) & ( for x being set holds ( x in B iff x is bag of X ) ) implies A = B ) assume that A3: for x being set holds ( x in A iff x is bag of X ) and A4: for x being set holds ( x in B iff x is bag of X ) ; ::_thesis: A = B now__::_thesis:_for_x_being_set_holds_ (_x_in_A_iff_x_in_B_) let x be set ; ::_thesis: ( x in A iff x in B ) ( x in A iff x is bag of X ) by A3; hence ( x in A iff x in B ) by A4; ::_thesis: verum end; hence A = B by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def12 defines Bags PRE_POLY:def_12_:_ for X being set for b2 being set holds ( b2 = Bags X iff for x being set holds ( x in b2 iff x is bag of X ) ); definition let X be set ; :: original: Bags redefine func Bags X -> Subset of (Bags X); coherence Bags X is Subset of (Bags X) proof Bags X c= Bags X ; hence Bags X is Subset of (Bags X) ; ::_thesis: verum end; end; theorem :: PRE_POLY:51 Bags {} = {{}} proof now__::_thesis:_for_x_being_set_holds_ (_(_x_in_{{}}_implies_x_is_bag_of_{}_)_&_(_x_is_bag_of_{}_implies_x_in_{{}}_)_) let x be set ; ::_thesis: ( ( x in {{}} implies x is bag of {} ) & ( x is bag of {} implies x in {{}} ) ) hereby ::_thesis: ( x is bag of {} implies x in {{}} ) assume x in {{}} ; ::_thesis: x is bag of {} then x = {} by TARSKI:def_1; hence x is bag of {} by PARTFUN1:def_2, RELAT_1:38, RELAT_1:def_18; ::_thesis: verum end; assume x is bag of {} ; ::_thesis: x in {{}} then reconsider x9 = x as ManySortedSet of {} ; x9 = {} ; hence x in {{}} by TARSKI:def_1; ::_thesis: verum end; hence Bags {} = {{}} by Def12; ::_thesis: verum end; registration let X be set ; cluster Bags X -> non empty ; coherence not Bags X is empty proof X --> 0 is bag of X by Th40; hence not Bags X is empty by Def12; ::_thesis: verum end; end; registration let X be set ; cluster -> functional for Element of bool (Bags X); coherence for b1 being Subset of (Bags X) holds b1 is functional proof let S be Subset of (Bags X); ::_thesis: S is functional let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in S or x is set ) thus ( not x in S or x is set ) by Def12; ::_thesis: verum end; end; registration let X be set ; let B be Subset of (Bags X); cluster -> X -defined for Element of B; coherence for b1 being Element of B holds b1 is X -defined proof let E be Element of B; ::_thesis: E is X -defined percases ( not B is empty or B is empty ) ; suppose not B is empty ; ::_thesis: E is X -defined then reconsider B = B as non empty Subset of (Bags X) ; reconsider E = E as Element of B ; E is bag of X by Def12; hence E is X -defined ; ::_thesis: verum end; suppose B is empty ; ::_thesis: E is X -defined then E is empty by SUBSET_1:def_1; hence E is X -defined by RELAT_1:171; ::_thesis: verum end; end; end; end; registration let X be set ; let B be non empty Subset of (Bags X); cluster -> total natural-valued finite-support for Element of B; coherence for b1 being Element of B holds ( b1 is total & b1 is natural-valued & b1 is finite-support ) by Def12; end; definition let X be set ; func EmptyBag X -> Element of Bags X equals :: PRE_POLY:def 13 X --> 0; coherence X --> 0 is Element of Bags X proof X --> 0 is bag of X by Th40; hence X --> 0 is Element of Bags X by Def12; ::_thesis: verum end; end; :: deftheorem defines EmptyBag PRE_POLY:def_13_:_ for X being set holds EmptyBag X = X --> 0; theorem Th52: :: PRE_POLY:52 for X, x being set holds (EmptyBag X) . x = 0 proof let X, x be set ; ::_thesis: (EmptyBag X) . x = 0 A1: dom (X --> 0) = X by FUNCOP_1:13; percases ( x in X or not x in X ) ; suppose x in X ; ::_thesis: (EmptyBag X) . x = 0 hence (EmptyBag X) . x = 0 by FUNCOP_1:7; ::_thesis: verum end; suppose not x in X ; ::_thesis: (EmptyBag X) . x = 0 hence (EmptyBag X) . x = 0 by A1, FUNCT_1:def_2; ::_thesis: verum end; end; end; theorem :: PRE_POLY:53 for X being set for b being bag of X holds b + (EmptyBag X) = b proof let X be set ; ::_thesis: for b being bag of X holds b + (EmptyBag X) = b let b be bag of X; ::_thesis: b + (EmptyBag X) = b now__::_thesis:_for_x_being_set_st_x_in_X_holds_ (b_+_(EmptyBag_X))_._x_=_b_._x let x be set ; ::_thesis: ( x in X implies (b + (EmptyBag X)) . x = b . x ) assume x in X ; ::_thesis: (b + (EmptyBag X)) . x = b . x then A1: (EmptyBag X) . x = 0 by FUNCOP_1:7; thus (b + (EmptyBag X)) . x = (b . x) + ((EmptyBag X) . x) by Def5 .= b . x by A1 ; ::_thesis: verum end; hence b + (EmptyBag X) = b by PBOOLE:3; ::_thesis: verum end; theorem Th54: :: PRE_POLY:54 for X being set for b being bag of X holds b -' (EmptyBag X) = b proof let X be set ; ::_thesis: for b being bag of X holds b -' (EmptyBag X) = b let b be bag of X; ::_thesis: b -' (EmptyBag X) = b now__::_thesis:_for_x_being_set_st_x_in_X_holds_ (b_-'_(EmptyBag_X))_._x_=_b_._x let x be set ; ::_thesis: ( x in X implies (b -' (EmptyBag X)) . x = b . x ) assume x in X ; ::_thesis: (b -' (EmptyBag X)) . x = b . x then A1: (EmptyBag X) . x = 0 by FUNCOP_1:7; thus (b -' (EmptyBag X)) . x = (b . x) -' ((EmptyBag X) . x) by Def6 .= b . x by A1, NAT_D:40 ; ::_thesis: verum end; hence b -' (EmptyBag X) = b by PBOOLE:3; ::_thesis: verum end; theorem :: PRE_POLY:55 for X being set for b being bag of X holds (EmptyBag X) -' b = EmptyBag X proof let X be set ; ::_thesis: for b being bag of X holds (EmptyBag X) -' b = EmptyBag X let b be bag of X; ::_thesis: (EmptyBag X) -' b = EmptyBag X now__::_thesis:_for_x_being_set_st_x_in_X_holds_ ((EmptyBag_X)_-'_b)_._x_=_(EmptyBag_X)_._x let x be set ; ::_thesis: ( x in X implies ((EmptyBag X) -' b) . x = (EmptyBag X) . x ) assume x in X ; ::_thesis: ((EmptyBag X) -' b) . x = (EmptyBag X) . x then A1: (EmptyBag X) . x = 0 by FUNCOP_1:7; thus ((EmptyBag X) -' b) . x = ((EmptyBag X) . x) -' (b . x) by Def6 .= (EmptyBag X) . x by A1, NAT_2:8 ; ::_thesis: verum end; hence (EmptyBag X) -' b = EmptyBag X by PBOOLE:3; ::_thesis: verum end; theorem Th56: :: PRE_POLY:56 for X being set for b being bag of X holds b -' b = EmptyBag X proof let X be set ; ::_thesis: for b being bag of X holds b -' b = EmptyBag X let b be bag of X; ::_thesis: b -' b = EmptyBag X now__::_thesis:_for_x_being_set_st_x_in_X_holds_ (b_-'_b)_._x_=_(EmptyBag_X)_._x let x be set ; ::_thesis: ( x in X implies (b -' b) . x = (EmptyBag X) . x ) assume x in X ; ::_thesis: (b -' b) . x = (EmptyBag X) . x thus (b -' b) . x = (b . x) -' (b . x) by Def6 .= 0 by XREAL_1:232 .= (EmptyBag X) . x by Th52 ; ::_thesis: verum end; hence b -' b = EmptyBag X by PBOOLE:3; ::_thesis: verum end; theorem Th57: :: PRE_POLY:57 for n being set for b1, b2 being bag of n st b1 divides b2 & b2 -' b1 = EmptyBag n holds b2 = b1 proof let n be set ; ::_thesis: for b1, b2 being bag of n st b1 divides b2 & b2 -' b1 = EmptyBag n holds b2 = b1 let b1, b2 be bag of n; ::_thesis: ( b1 divides b2 & b2 -' b1 = EmptyBag n implies b2 = b1 ) assume that A1: b1 divides b2 and A2: b2 -' b1 = EmptyBag n ; ::_thesis: b2 = b1 now__::_thesis:_for_k_being_set_st_k_in_n_holds_ b2_._k_=_b1_._k let k be set ; ::_thesis: ( k in n implies b2 . k = b1 . k ) assume k in n ; ::_thesis: b2 . k = b1 . k 0 = (b2 -' b1) . k by A2, Th52 .= (b2 . k) -' (b1 . k) by Def6 ; then A3: b2 . k <= b1 . k by NAT_D:36; b1 . k <= b2 . k by A1, Def11; hence b2 . k = b1 . k by A3, XXREAL_0:1; ::_thesis: verum end; hence b2 = b1 by PBOOLE:3; ::_thesis: verum end; theorem Th58: :: PRE_POLY:58 for n being set for b being bag of n st b divides EmptyBag n holds EmptyBag n = b proof let n be set ; ::_thesis: for b being bag of n st b divides EmptyBag n holds EmptyBag n = b let b be bag of n; ::_thesis: ( b divides EmptyBag n implies EmptyBag n = b ) assume A1: b divides EmptyBag n ; ::_thesis: EmptyBag n = b now__::_thesis:_for_k_being_set_st_k_in_n_holds_ (EmptyBag_n)_._k_=_b_._k let k be set ; ::_thesis: ( k in n implies (EmptyBag n) . k = b . k ) assume k in n ; ::_thesis: (EmptyBag n) . k = b . k (EmptyBag n) . k = 0 by Th52; hence (EmptyBag n) . k = b . k by A1, Def11; ::_thesis: verum end; hence EmptyBag n = b by PBOOLE:3; ::_thesis: verum end; theorem Th59: :: PRE_POLY:59 for n being set for b being bag of n holds EmptyBag n divides b proof let n be set ; ::_thesis: for b being bag of n holds EmptyBag n divides b let b be bag of n; ::_thesis: EmptyBag n divides b let k be set ; :: according to PRE_POLY:def_11 ::_thesis: (EmptyBag n) . k <= b . k thus (EmptyBag n) . k <= b . k by Th52; ::_thesis: verum end; theorem :: PRE_POLY:60 for n being Ordinal for b being bag of n holds EmptyBag n <=' b by Th49, Th59; definition let n be Ordinal; func BagOrder n -> Order of (Bags n) means :Def14: :: PRE_POLY:def 14 for p, q being bag of n holds ( [p,q] in it iff p <=' q ); existence ex b1 being Order of (Bags n) st for p, q being bag of n holds ( [p,q] in b1 iff p <=' q ) proof defpred S1[ set , set ] means ex b1, b2 being Element of Bags n st ( $1 = b1 & $2 = b2 & b1 <=' b2 ); consider BO being Relation of (Bags n),(Bags n) such that A1: for x, y being set holds ( [x,y] in BO iff ( x in Bags n & y in Bags n & S1[x,y] ) ) from RELSET_1:sch_1(); A2: BO is_antisymmetric_in Bags n proof let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in Bags n or not y in Bags n or not [x,y] in BO or not [y,x] in BO or x = y ) assume that x in Bags n and y in Bags n and A3: [x,y] in BO and A4: [y,x] in BO ; ::_thesis: x = y A5: ex b19, b29 being Element of Bags n st ( y = b19 & x = b29 & b19 <=' b29 ) by A1, A4; consider b1, b2 being Element of Bags n such that A6: ( x = b1 & y = b2 ) and A7: b1 <=' b2 by A1, A3; ( b1 < b2 or b1 = b2 ) by A7, Def10; hence x = y by A6, A5, Def10; ::_thesis: verum end; A8: BO is_reflexive_in Bags n proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in Bags n or [x,x] in BO ) assume x in Bags n ; ::_thesis: [x,x] in BO hence [x,x] in BO by A1; ::_thesis: verum end; then A9: ( dom BO = Bags n & field BO = Bags n ) by ORDERS_1:13; BO is_transitive_in Bags n proof let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in Bags n or not y in Bags n or not z in Bags n or not [x,y] in BO or not [y,z] in BO or [x,z] in BO ) assume that x in Bags n and y in Bags n and z in Bags n and A10: [x,y] in BO and A11: [y,z] in BO ; ::_thesis: [x,z] in BO consider b1, b2 being Element of Bags n such that A12: x = b1 and A13: ( y = b2 & b1 <=' b2 ) by A1, A10; consider b19, b29 being Element of Bags n such that A14: y = b19 and A15: z = b29 and A16: b19 <=' b29 by A1, A11; reconsider B1 = b1, B29 = b29 as bag of n ; B1 <=' B29 by A13, A14, A16, Th42; hence [x,z] in BO by A1, A12, A15; ::_thesis: verum end; then reconsider BO = BO as Order of (Bags n) by A8, A2, A9, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_16; take BO ; ::_thesis: for p, q being bag of n holds ( [p,q] in BO iff p <=' q ) let p, q be bag of n; ::_thesis: ( [p,q] in BO iff p <=' q ) hereby ::_thesis: ( p <=' q implies [p,q] in BO ) assume [p,q] in BO ; ::_thesis: p <=' q then ex b1, b2 being Element of Bags n st ( p = b1 & q = b2 & b1 <=' b2 ) by A1; hence p <=' q ; ::_thesis: verum end; ( p in Bags n & q in Bags n ) by Def12; hence ( p <=' q implies [p,q] in BO ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Order of (Bags n) st ( for p, q being bag of n holds ( [p,q] in b1 iff p <=' q ) ) & ( for p, q being bag of n holds ( [p,q] in b2 iff p <=' q ) ) holds b1 = b2 proof let B1, B2 be Order of (Bags n); ::_thesis: ( ( for p, q being bag of n holds ( [p,q] in B1 iff p <=' q ) ) & ( for p, q being bag of n holds ( [p,q] in B2 iff p <=' q ) ) implies B1 = B2 ) assume that A17: for p, q being bag of n holds ( [p,q] in B1 iff p <=' q ) and A18: for p, q being bag of n holds ( [p,q] in B2 iff p <=' q ) ; ::_thesis: B1 = B2 let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in B1 or [a,b] in B2 ) & ( not [a,b] in B2 or [a,b] in B1 ) ) hereby ::_thesis: ( not [a,b] in B2 or [a,b] in B1 ) assume A19: [a,b] in B1 ; ::_thesis: [a,b] in B2 then consider b1, b2 being set such that A20: [a,b] = [b1,b2] and A21: ( b1 in Bags n & b2 in Bags n ) by RELSET_1:2; reconsider b1 = b1, b2 = b2 as bag of n by A21; b1 <=' b2 by A17, A19, A20; hence [a,b] in B2 by A18, A20; ::_thesis: verum end; assume A22: [a,b] in B2 ; ::_thesis: [a,b] in B1 then consider b1, b2 being set such that A23: [a,b] = [b1,b2] and A24: ( b1 in Bags n & b2 in Bags n ) by RELSET_1:2; reconsider b1 = b1, b2 = b2 as bag of n by A24; b1 <=' b2 by A18, A22, A23; hence [a,b] in B1 by A17, A23; ::_thesis: verum end; end; :: deftheorem Def14 defines BagOrder PRE_POLY:def_14_:_ for n being Ordinal for b2 being Order of (Bags n) holds ( b2 = BagOrder n iff for p, q being bag of n holds ( [p,q] in b2 iff p <=' q ) ); Lm1: for n being Ordinal holds BagOrder n is_reflexive_in Bags n proof let n be Ordinal; ::_thesis: BagOrder n is_reflexive_in Bags n let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in Bags n or [x,x] in BagOrder n ) assume x in Bags n ; ::_thesis: [x,x] in BagOrder n then reconsider x9 = x as bag of n ; x9 <=' x9 ; hence [x,x] in BagOrder n by Def14; ::_thesis: verum end; Lm2: for n being Ordinal holds BagOrder n is_antisymmetric_in Bags n proof let n be Ordinal; ::_thesis: BagOrder n is_antisymmetric_in Bags n set BO = BagOrder n; let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in Bags n or not y in Bags n or not [x,y] in BagOrder n or not [y,x] in BagOrder n or x = y ) assume that A1: ( x in Bags n & y in Bags n ) and A2: [x,y] in BagOrder n and A3: [y,x] in BagOrder n ; ::_thesis: x = y reconsider b1 = x, b2 = y as bag of n by A1; b1 <=' b2 by A2, Def14; then A4: ( b1 < b2 or b1 = b2 ) by Def10; reconsider b19 = y, b29 = x as bag of n by A1; b19 <=' b29 by A3, Def14; hence x = y by A4, Def10; ::_thesis: verum end; Lm3: for n being Ordinal holds BagOrder n is_transitive_in Bags n proof let n be Ordinal; ::_thesis: BagOrder n is_transitive_in Bags n set BO = BagOrder n; let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in Bags n or not y in Bags n or not z in Bags n or not [x,y] in BagOrder n or not [y,z] in BagOrder n or [x,z] in BagOrder n ) assume that A1: x in Bags n and A2: y in Bags n and A3: z in Bags n and A4: ( [x,y] in BagOrder n & [y,z] in BagOrder n ) ; ::_thesis: [x,z] in BagOrder n reconsider b19 = y, b29 = z as bag of n by A2, A3; reconsider b1 = x, b2 = y as bag of n by A1, A2; reconsider B1 = b1, B29 = b29 as bag of n ; ( b1 <=' b2 & b19 <=' b29 ) by A4, Def14; then B1 <=' B29 by Th42; hence [x,z] in BagOrder n by Def14; ::_thesis: verum end; Lm4: for n being Ordinal holds BagOrder n linearly_orders Bags n proof let n be Ordinal; ::_thesis: BagOrder n linearly_orders Bags n set BO = BagOrder n; A1: BagOrder n is_transitive_in Bags n by Lm3; A2: BagOrder n is_connected_in Bags n proof let x, y be set ; :: according to RELAT_2:def_6 ::_thesis: ( not x in Bags n or not y in Bags n or x = y or [x,y] in BagOrder n or [y,x] in BagOrder n ) assume that A3: ( x in Bags n & y in Bags n ) and x <> y and A4: not [x,y] in BagOrder n ; ::_thesis: [y,x] in BagOrder n reconsider p = x, q = y as bag of n by A3; not p <=' q by A4, Def14; then q <=' p by Th45; hence [y,x] in BagOrder n by Def14; ::_thesis: verum end; ( BagOrder n is_reflexive_in Bags n & BagOrder n is_antisymmetric_in Bags n ) by Lm1, Lm2; hence BagOrder n linearly_orders Bags n by A1, A2, ORDERS_1:def_8; ::_thesis: verum end; registration let n be Ordinal; cluster BagOrder n -> being_linear-order ; coherence BagOrder n is being_linear-order proof set BO = BagOrder n; BagOrder n linearly_orders Bags n by Lm4; then ( field (BagOrder n) = Bags n & BagOrder n is_connected_in Bags n ) by ORDERS_1:15, ORDERS_1:def_8; then BagOrder n is connected by RELAT_2:def_14; hence BagOrder n is being_linear-order by ORDERS_1:def_5; ::_thesis: verum end; end; definition let X be set ; let f be Function of X,NAT; func NatMinor f -> Subset of (Funcs (X,NAT)) means :Def15: :: PRE_POLY:def 15 for g being natural-valued ManySortedSet of X holds ( g in it iff for x being set st x in X holds g . x <= f . x ); existence ex b1 being Subset of (Funcs (X,NAT)) st for g being natural-valued ManySortedSet of X holds ( g in b1 iff for x being set st x in X holds g . x <= f . x ) proof defpred S1[ set ] means ex g being natural-valued ManySortedSet of X st ( $1 = g & ( for x being set st x in X holds g . x <= f . x ) ); consider IT being Subset of (Funcs (X,NAT)) such that A1: for h being set holds ( h in IT iff ( h in Funcs (X,NAT) & S1[h] ) ) from SUBSET_1:sch_1(); take IT ; ::_thesis: for g being natural-valued ManySortedSet of X holds ( g in IT iff for x being set st x in X holds g . x <= f . x ) let g be natural-valued ManySortedSet of X; ::_thesis: ( g in IT iff for x being set st x in X holds g . x <= f . x ) hereby ::_thesis: ( ( for x being set st x in X holds g . x <= f . x ) implies g in IT ) assume g in IT ; ::_thesis: for x being set st x in X holds g . x <= f . x then ex g1 being natural-valued ManySortedSet of X st ( g1 = g & ( for x being set st x in X holds g1 . x <= f . x ) ) by A1; hence for x being set st x in X holds g . x <= f . x ; ::_thesis: verum end; ( dom g = X & rng g c= NAT ) by PARTFUN1:def_2, VALUED_0:def_6; then g is Function of X,NAT by RELSET_1:4; then A2: g in Funcs (X,NAT) by FUNCT_2:8; assume for x being set st x in X holds g . x <= f . x ; ::_thesis: g in IT hence g in IT by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (Funcs (X,NAT)) st ( for g being natural-valued ManySortedSet of X holds ( g in b1 iff for x being set st x in X holds g . x <= f . x ) ) & ( for g being natural-valued ManySortedSet of X holds ( g in b2 iff for x being set st x in X holds g . x <= f . x ) ) holds b1 = b2 proof let it1, it2 be Subset of (Funcs (X,NAT)); ::_thesis: ( ( for g being natural-valued ManySortedSet of X holds ( g in it1 iff for x being set st x in X holds g . x <= f . x ) ) & ( for g being natural-valued ManySortedSet of X holds ( g in it2 iff for x being set st x in X holds g . x <= f . x ) ) implies it1 = it2 ) assume that A3: for g being natural-valued ManySortedSet of X holds ( g in it1 iff for x being set st x in X holds g . x <= f . x ) and A4: for g being natural-valued ManySortedSet of X holds ( g in it2 iff for x being set st x in X holds g . x <= f . x ) ; ::_thesis: it1 = it2 now__::_thesis:_for_h_being_Element_of_Funcs_(X,NAT)_holds_ (_(_h_in_it1_implies_h_in_it2_)_&_(_h_in_it2_implies_h_in_it1_)_) let h be Element of Funcs (X,NAT); ::_thesis: ( ( h in it1 implies h in it2 ) & ( h in it2 implies h in it1 ) ) hereby ::_thesis: ( h in it2 implies h in it1 ) assume h in it1 ; ::_thesis: h in it2 then for x being set st x in X holds h . x <= f . x by A3; hence h in it2 by A4; ::_thesis: verum end; assume h in it2 ; ::_thesis: h in it1 then for x being set st x in X holds h . x <= f . x by A4; hence h in it1 by A3; ::_thesis: verum end; hence it1 = it2 by SUBSET_1:3; ::_thesis: verum end; end; :: deftheorem Def15 defines NatMinor PRE_POLY:def_15_:_ for X being set for f being Function of X,NAT for b3 being Subset of (Funcs (X,NAT)) holds ( b3 = NatMinor f iff for g being natural-valued ManySortedSet of X holds ( g in b3 iff for x being set st x in X holds g . x <= f . x ) ); theorem Th61: :: PRE_POLY:61 for X being set for f being Function of X,NAT holds f in NatMinor f proof let X be set ; ::_thesis: for f being Function of X,NAT holds f in NatMinor f let f be Function of X,NAT; ::_thesis: f in NatMinor f for x being set st x in X holds f . x <= f . x ; hence f in NatMinor f by Def15; ::_thesis: verum end; registration let X be set ; let f be Function of X,NAT; cluster NatMinor f -> functional non empty ; coherence ( not NatMinor f is empty & NatMinor f is functional ) by Th61; end; registration let X be set ; let f be Function of X,NAT; cluster -> natural-valued for Element of NatMinor f; coherence for b1 being Element of NatMinor f holds b1 is natural-valued proof let x be Element of NatMinor f; ::_thesis: x is natural-valued rng x c= NAT by FUNCT_2:92; hence x is natural-valued by VALUED_0:def_6; ::_thesis: verum end; end; theorem Th62: :: PRE_POLY:62 for X being set for f being finite-support Function of X,NAT holds NatMinor f c= Bags X proof let X be set ; ::_thesis: for f being finite-support Function of X,NAT holds NatMinor f c= Bags X let f be finite-support Function of X,NAT; ::_thesis: NatMinor f c= Bags X let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NatMinor f or x in Bags X ) assume x in NatMinor f ; ::_thesis: x in Bags X then reconsider x9 = x as Element of NatMinor f ; A1: dom x9 = X by FUNCT_2:92; then A2: x9 is ManySortedSet of X by PARTFUN1:def_2, RELAT_1:def_18; support x9 c= support f proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in support x9 or a in support f ) A3: support x9 c= dom x9 by Th37; assume A4: a in support x9 ; ::_thesis: a in support f then x9 . a <> 0 by Def7; then f . a <> 0 by A1, A2, A4, A3, Def15; hence a in support f by Def7; ::_thesis: verum end; then x is bag of X by A1, Def8, PARTFUN1:def_2, RELAT_1:def_18; hence x in Bags X by Def12; ::_thesis: verum end; definition let X be set ; let f be finite-support Function of X,NAT; :: original: support redefine func support f -> Element of Fin X; coherence support f is Element of Fin X proof dom f = X by FUNCT_2:def_1; then support f c= X by Th37; hence support f is Element of Fin X by FINSUB_1:def_5; ::_thesis: verum end; end; theorem Th63: :: PRE_POLY:63 for X being non empty set for f being finite-support Function of X,NAT holds card (NatMinor f) = multnat $$ ((support f),(addnat [:] (f,1))) proof let X be non empty set ; ::_thesis: for f being finite-support Function of X,NAT holds card (NatMinor f) = multnat $$ ((support f),(addnat [:] (f,1))) defpred S1[ Element of Fin X] means for f being Function of X,NAT st ( for x being Element of X st not x in $1 holds f . x = 0 ) holds card (NatMinor f) = multnat $$ ($1,(addnat [:] (f,1))); let f be finite-support Function of X,NAT; ::_thesis: card (NatMinor f) = multnat $$ ((support f),(addnat [:] (f,1))) A1: for x being Element of X st not x in support f holds f . x = 0 by Def7; A2: for B being Element of Fin X for b being Element of X st S1[B] & not b in B holds S1[B \/ {.b.}] proof let B be Element of Fin X; ::_thesis: for b being Element of X st S1[B] & not b in B holds S1[B \/ {.b.}] let b be Element of X; ::_thesis: ( S1[B] & not b in B implies S1[B \/ {.b.}] ) assume that A3: S1[B] and A4: not b in B ; ::_thesis: S1[B \/ {.b.}] let f be Function of X,NAT; ::_thesis: ( ( for x being Element of X st not x in B \/ {.b.} holds f . x = 0 ) implies card (NatMinor f) = multnat $$ ((B \/ {.b.}),(addnat [:] (f,1))) ) assume A5: for x being Element of X st not x in B \/ {b} holds f . x = 0 ; ::_thesis: card (NatMinor f) = multnat $$ ((B \/ {.b.}),(addnat [:] (f,1))) set g = f +* (b,0); (f +* (b,0)) | B = f | B by A4, FUNCT_7:92; then (addnat [:] ((f +* (b,0)),1)) | B = (addnat [:] (f,1)) | B by FUNCOP_1:28; then A6: multnat $$ (B,(addnat [:] ((f +* (b,0)),1))) = multnat $$ (B,(addnat [:] (f,1))) by SETWOP_2:7; A7: dom f = X by FUNCT_2:def_1; for x being Element of X st not x in B holds (f +* (b,0)) . x = 0 proof let x be Element of X; ::_thesis: ( not x in B implies (f +* (b,0)) . x = 0 ) assume A8: not x in B ; ::_thesis: (f +* (b,0)) . x = 0 percases ( x = b or x <> b ) ; suppose x = b ; ::_thesis: (f +* (b,0)) . x = 0 hence (f +* (b,0)) . x = 0 by A7, FUNCT_7:31; ::_thesis: verum end; supposeA9: x <> b ; ::_thesis: (f +* (b,0)) . x = 0 A10: now__::_thesis:_not_x_in_B_\/_{b} assume x in B \/ {b} ; ::_thesis: contradiction then ( x in B or x in {b} ) by XBOOLE_0:def_3; hence contradiction by A8, A9, TARSKI:def_1; ::_thesis: verum end; thus (f +* (b,0)) . x = f . x by A9, FUNCT_7:32 .= 0 by A5, A10 ; ::_thesis: verum end; end; end; then A11: card (NatMinor (f +* (b,0))) = multnat $$ (B,(addnat [:] ((f +* (b,0)),1))) by A3; then reconsider ng = NatMinor (f +* (b,0)) as functional non empty finite set ; reconsider fb1 = (f . b) + 1 as non empty Element of NAT ; dom (addnat [:] (f,1)) = X by FUNCT_2:def_1; then A12: (addnat [:] (f,1)) . b = addnat . ((f . b),1) by FUNCOP_1:27 .= (f . b) + 1 by BINOP_2:def_23 ; set cng = card ng; A13: f . b < (f . b) + 1 by XREAL_1:29; [:ng,((f . b) + 1):], NatMinor f are_equipotent proof deffunc H1( Element of ng, Element of fb1) -> set = $1 +* (b,$2); A14: for p being Element of ng for l being Element of fb1 holds H1(p,l) in NatMinor f proof let p be Element of ng; ::_thesis: for l being Element of fb1 holds H1(p,l) in NatMinor f let l be Element of fb1; ::_thesis: H1(p,l) in NatMinor f reconsider q = p as Element of NatMinor (f +* (b,0)) ; ( fb1 c= NAT & l in fb1 ) ; then reconsider k = l as Element of NAT ; p in NatMinor (f +* (b,0)) ; then A15: dom p = X by FUNCT_2:92; then dom (p +* (b,l)) = X by FUNCT_7:30; then reconsider pbl = q +* (b,k) as natural-valued ManySortedSet of X by PARTFUN1:def_2, RELAT_1:def_18; for x being set st x in X holds pbl . x <= f . x proof let x be set ; ::_thesis: ( x in X implies pbl . x <= f . x ) assume A16: x in X ; ::_thesis: pbl . x <= f . x percases ( x = b or x <> b ) ; supposeA17: x = b ; ::_thesis: pbl . x <= f . x A18: k < fb1 by NAT_1:44; pbl . x = k by A15, A17, FUNCT_7:31; hence pbl . x <= f . x by A17, A18, NAT_1:13; ::_thesis: verum end; supposeA19: x <> b ; ::_thesis: pbl . x <= f . x q is ManySortedSet of X by A15, PARTFUN1:def_2, RELAT_1:def_18; then A20: q . x <= (f +* (b,0)) . x by A16, Def15; pbl . x = q . x by A19, FUNCT_7:32; hence pbl . x <= f . x by A19, A20, FUNCT_7:32; ::_thesis: verum end; end; end; hence H1(p,l) in NatMinor f by Def15; ::_thesis: verum end; consider r being Function of [:ng,fb1:],(NatMinor f) such that A21: for p being Element of ng for l being Element of fb1 holds r . (p,l) = H1(p,l) from FUNCT_7:sch_1(A14); take r ; :: according to WELLORD2:def_4 ::_thesis: ( r is one-to-one & dom r = [:ng,((f . b) + 1):] & rng r = NatMinor f ) thus r is one-to-one ::_thesis: ( dom r = [:ng,((f . b) + 1):] & rng r = NatMinor f ) proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom r or not x2 in dom r or not r . x1 = r . x2 or x1 = x2 ) assume that A22: x1 in dom r and A23: x2 in dom r and A24: r . x1 = r . x2 ; ::_thesis: x1 = x2 consider p2, l2 being set such that A25: x2 = [p2,l2] by A23, RELAT_1:def_1; reconsider p2 = p2 as Element of NatMinor (f +* (b,0)) by A23, A25, ZFMISC_1:87; A26: dom p2 = X by FUNCT_2:92; A27: l2 in fb1 by A23, A25, ZFMISC_1:87; consider p1, l1 being set such that A28: x1 = [p1,l1] by A22, RELAT_1:def_1; reconsider p1 = p1 as Element of NatMinor (f +* (b,0)) by A22, A28, ZFMISC_1:87; A29: dom p1 = X by FUNCT_2:92; then reconsider p19 = p1, p29 = p2 as natural-valued ManySortedSet of X by A26, PARTFUN1:def_2, RELAT_1:def_18; l1 in fb1 by A22, A28, ZFMISC_1:87; then A30: p1 +* (b,l1) = r . (p1,l1) by A21 .= r . (p2,l2) by A24, A28, A25 .= p2 +* (b,l2) by A21, A27 ; A31: now__::_thesis:_for_x_being_set_st_x_in_X_holds_ p19_._x_=_p29_._x let x be set ; ::_thesis: ( x in X implies p19 . b1 = p29 . b1 ) assume x in X ; ::_thesis: p19 . b1 = p29 . b1 percases ( x = b or x <> b ) ; supposeA32: x = b ; ::_thesis: p19 . b1 = p29 . b1 A33: (f +* (b,0)) . b = 0 by A7, FUNCT_7:31; hence p19 . x = 0 by A32, Def15 .= p29 . x by A32, A33, Def15 ; ::_thesis: verum end; supposeA34: x <> b ; ::_thesis: p19 . b1 = p29 . b1 hence p19 . x = (p1 +* (b,l1)) . x by FUNCT_7:32 .= p29 . x by A30, A34, FUNCT_7:32 ; ::_thesis: verum end; end; end; l1 = (p1 +* (b,l1)) . b by A29, FUNCT_7:31 .= l2 by A30, A26, FUNCT_7:31 ; hence x1 = x2 by A28, A25, A31, PBOOLE:3; ::_thesis: verum end; thus A35: dom r = [:ng,((f . b) + 1):] by FUNCT_2:def_1; ::_thesis: rng r = NatMinor f thus rng r c= NatMinor f ; :: according to XBOOLE_0:def_10 ::_thesis: NatMinor f c= rng r thus NatMinor f c= rng r ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NatMinor f or x in rng r ) assume x in NatMinor f ; ::_thesis: x in rng r then reconsider e = x as Element of NatMinor f ; A36: dom e = X by FUNCT_2:92; then dom (e +* (b,0)) = X by FUNCT_7:30; then reconsider eb0 = e +* (b,0) as natural-valued ManySortedSet of X by PARTFUN1:def_2, RELAT_1:def_18; A37: e is ManySortedSet of X by A36, PARTFUN1:def_2, RELAT_1:def_18; now__::_thesis:_for_x_being_set_st_x_in_X_holds_ eb0_._x_<=_(f_+*_(b,0))_._x let x be set ; ::_thesis: ( x in X implies eb0 . b1 <= (f +* (b,0)) . b1 ) assume A38: x in X ; ::_thesis: eb0 . b1 <= (f +* (b,0)) . b1 percases ( x = b or x <> b ) ; suppose x = b ; ::_thesis: eb0 . b1 <= (f +* (b,0)) . b1 hence eb0 . x <= (f +* (b,0)) . x by A36, FUNCT_7:31; ::_thesis: verum end; supposeA39: x <> b ; ::_thesis: eb0 . b1 <= (f +* (b,0)) . b1 then A40: eb0 . x = e . x by FUNCT_7:32; e . x <= f . x by A37, A38, Def15; hence eb0 . x <= (f +* (b,0)) . x by A39, A40, FUNCT_7:32; ::_thesis: verum end; end; end; then reconsider eb0 = eb0 as Element of NatMinor (f +* (b,0)) by Def15; e . b <= f . b by A37, Def15; then e . b < fb1 by A13, XXREAL_0:2; then A41: e . b in fb1 by NAT_1:44; then A42: [eb0,(e . b)] in dom r by A35, ZFMISC_1:87; e = e +* (b,(e . b)) by FUNCT_7:35 .= eb0 +* (b,(e . b)) by FUNCT_7:34 ; then e = r . (eb0,(e . b)) by A21, A41; hence x in rng r by A42, FUNCT_1:def_3; ::_thesis: verum end; end; hence card (NatMinor f) = card [:ng,((f . b) + 1):] by CARD_1:5 .= (card ng) * (card ((f . b) + 1)) by CARD_2:46 .= (card ng) * ((f . b) + 1) by CARD_1:def_2 .= multnat . ((multnat $$ (B,(addnat [:] (f,1)))),((f . b) + 1)) by A11, A6, BINOP_2:def_24 .= multnat $$ ((B \/ {.b.}),(addnat [:] (f,1))) by A4, A12, SETWOP_2:2 ; ::_thesis: verum end; A43: S1[ {}. X] proof let f be Function of X,NAT; ::_thesis: ( ( for x being Element of X st not x in {}. X holds f . x = 0 ) implies card (NatMinor f) = multnat $$ (({}. X),(addnat [:] (f,1))) ) assume A44: for x being Element of X st not x in {}. X holds f . x = 0 ; ::_thesis: card (NatMinor f) = multnat $$ (({}. X),(addnat [:] (f,1))) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_NatMinor_f_implies_x_=_f_)_&_(_x_=_f_implies_x_in_NatMinor_f_)_) let x be set ; ::_thesis: ( ( x in NatMinor f implies x = f ) & ( x = f implies x in NatMinor f ) ) hereby ::_thesis: ( x = f implies x in NatMinor f ) assume A45: x in NatMinor f ; ::_thesis: x = f then reconsider x9 = x as Function of X,NAT by FUNCT_2:66; now__::_thesis:_for_c_being_Element_of_X_holds_x9_._c_=_f_._c let c be Element of X; ::_thesis: x9 . c = f . c f . c = 0 by A44; hence x9 . c = f . c by A45, Def15; ::_thesis: verum end; hence x = f by FUNCT_2:63; ::_thesis: verum end; thus ( x = f implies x in NatMinor f ) by Th61; ::_thesis: verum end; then NatMinor f = {f} by TARSKI:def_1; hence card (NatMinor f) = 1 by CARD_1:30 .= multnat $$ (({}. X),(addnat [:] (f,1))) by BINOP_2:10, SETWISEO:31 ; ::_thesis: verum end; for B being Element of Fin X holds S1[B] from SETWISEO:sch_2(A43, A2); hence card (NatMinor f) = multnat $$ ((support f),(addnat [:] (f,1))) by A1; ::_thesis: verum end; registration let X be set ; let f be finite-support Function of X,NAT; cluster NatMinor f -> finite ; coherence NatMinor f is finite proof percases ( X is empty or not X is empty ) ; suppose X is empty ; ::_thesis: NatMinor f is finite then NatMinor f c= Funcs ({},NAT) ; then NatMinor f c= {{}} by FUNCT_5:57; hence NatMinor f is finite ; ::_thesis: verum end; suppose not X is empty ; ::_thesis: NatMinor f is finite then reconsider X = X as non empty set ; reconsider f = f as finite-support Function of X,NAT ; card (NatMinor f) = multnat $$ ((support f),(addnat [:] (f,1))) by Th63; hence NatMinor f is finite ; ::_thesis: verum end; end; end; end; definition let n be Ordinal; let b be bag of n; func divisors b -> FinSequence of Bags n means :Def16: :: PRE_POLY:def 16 ex S being non empty finite Subset of (Bags n) st ( it = SgmX ((BagOrder n),S) & ( for p being bag of n holds ( p in S iff p divides b ) ) ); existence ex b1 being FinSequence of Bags n ex S being non empty finite Subset of (Bags n) st ( b1 = SgmX ((BagOrder n),S) & ( for p being bag of n holds ( p in S iff p divides b ) ) ) proof ( dom b = n & rng b c= NAT ) by PARTFUN1:def_2, VALUED_0:def_6; then reconsider f = b as finite-support Function of n,NAT by RELSET_1:4; reconsider S = NatMinor f as non empty finite Subset of (Bags n) by Th62; take IT = SgmX ((BagOrder n),S); ::_thesis: ex S being non empty finite Subset of (Bags n) st ( IT = SgmX ((BagOrder n),S) & ( for p being bag of n holds ( p in S iff p divides b ) ) ) take S ; ::_thesis: ( IT = SgmX ((BagOrder n),S) & ( for p being bag of n holds ( p in S iff p divides b ) ) ) thus IT = SgmX ((BagOrder n),S) ; ::_thesis: for p being bag of n holds ( p in S iff p divides b ) let p be bag of n; ::_thesis: ( p in S iff p divides b ) thus ( p in S implies p divides b ) ::_thesis: ( p divides b implies p in S ) proof assume p in S ; ::_thesis: p divides b then for x being set st x in n holds p . x <= b . x by Def15; hence p divides b by Th46; ::_thesis: verum end; assume p divides b ; ::_thesis: p in S then for x being set st x in n holds p . x <= b . x by Def11; hence p in S by Def15; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of Bags n st ex S being non empty finite Subset of (Bags n) st ( b1 = SgmX ((BagOrder n),S) & ( for p being bag of n holds ( p in S iff p divides b ) ) ) & ex S being non empty finite Subset of (Bags n) st ( b2 = SgmX ((BagOrder n),S) & ( for p being bag of n holds ( p in S iff p divides b ) ) ) holds b1 = b2 proof let it1, it2 be FinSequence of Bags n; ::_thesis: ( ex S being non empty finite Subset of (Bags n) st ( it1 = SgmX ((BagOrder n),S) & ( for p being bag of n holds ( p in S iff p divides b ) ) ) & ex S being non empty finite Subset of (Bags n) st ( it2 = SgmX ((BagOrder n),S) & ( for p being bag of n holds ( p in S iff p divides b ) ) ) implies it1 = it2 ) given S1 being non empty finite Subset of (Bags n) such that A1: it1 = SgmX ((BagOrder n),S1) and A2: for p being bag of n holds ( p in S1 iff p divides b ) ; ::_thesis: ( for S being non empty finite Subset of (Bags n) holds ( not it2 = SgmX ((BagOrder n),S) or ex p being bag of n st ( ( p in S implies p divides b ) implies ( p divides b & not p in S ) ) ) or it1 = it2 ) given S2 being non empty finite Subset of (Bags n) such that A3: it2 = SgmX ((BagOrder n),S2) and A4: for p being bag of n holds ( p in S2 iff p divides b ) ; ::_thesis: it1 = it2 now__::_thesis:_for_x_being_set_holds_ (_(_x_in_S1_implies_x_in_S2_)_&_(_x_in_S2_implies_x_in_S1_)_) let x be set ; ::_thesis: ( ( x in S1 implies x in S2 ) & ( x in S2 implies x in S1 ) ) hereby ::_thesis: ( x in S2 implies x in S1 ) assume A5: x in S1 ; ::_thesis: x in S2 then reconsider x9 = x as Element of Bags n ; x9 divides b by A2, A5; hence x in S2 by A4; ::_thesis: verum end; assume A6: x in S2 ; ::_thesis: x in S1 then reconsider x9 = x as Element of Bags n ; x9 divides b by A4, A6; hence x in S1 by A2; ::_thesis: verum end; hence it1 = it2 by A1, A3, TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def16 defines divisors PRE_POLY:def_16_:_ for n being Ordinal for b being bag of n for b3 being FinSequence of Bags n holds ( b3 = divisors b iff ex S being non empty finite Subset of (Bags n) st ( b3 = SgmX ((BagOrder n),S) & ( for p being bag of n holds ( p in S iff p divides b ) ) ) ); registration let n be Ordinal; let b be bag of n; cluster divisors b -> one-to-one non empty ; coherence ( not divisors b is empty & divisors b is one-to-one ) proof ex S being non empty finite Subset of (Bags n) st ( divisors b = SgmX ((BagOrder n),S) & ( for p being bag of n holds ( p in S iff p divides b ) ) ) by Def16; hence ( not divisors b is empty & divisors b is one-to-one ) ; ::_thesis: verum end; end; theorem Th64: :: PRE_POLY:64 for n being Ordinal for i being Element of NAT for b being bag of n st i in dom (divisors b) holds (divisors b) /. i divides b proof let n be Ordinal; ::_thesis: for i being Element of NAT for b being bag of n st i in dom (divisors b) holds (divisors b) /. i divides b let i be Element of NAT ; ::_thesis: for b being bag of n st i in dom (divisors b) holds (divisors b) /. i divides b let b be bag of n; ::_thesis: ( i in dom (divisors b) implies (divisors b) /. i divides b ) assume i in dom (divisors b) ; ::_thesis: (divisors b) /. i divides b then A1: ( (divisors b) /. i = (divisors b) . i & (divisors b) . i in rng (divisors b) ) by FUNCT_1:def_3, PARTFUN1:def_6; reconsider pid = (divisors b) /. i as bag of n ; consider S being non empty finite Subset of (Bags n) such that A2: divisors b = SgmX ((BagOrder n),S) and A3: for p being bag of n holds ( p in S iff p divides b ) by Def16; BagOrder n linearly_orders S by Lm4, ORDERS_1:38; then pid in S by A2, A1, Def2; hence (divisors b) /. i divides b by A3; ::_thesis: verum end; theorem Th65: :: PRE_POLY:65 for n being Ordinal for b being bag of n holds ( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b ) proof let n be Ordinal; ::_thesis: for b being bag of n holds ( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b ) let b be bag of n; ::_thesis: ( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b ) consider S being non empty finite Subset of (Bags n) such that A1: divisors b = SgmX ((BagOrder n),S) and A2: for p being bag of n holds ( p in S iff p divides b ) by Def16; A3: now__::_thesis:_for_y_being_Element_of_Bags_n_st_y_in_S_holds_ [y,b]_in_BagOrder_n let y be Element of Bags n; ::_thesis: ( y in S implies [y,b] in BagOrder n ) assume y in S ; ::_thesis: [y,b] in BagOrder n then y divides b by A2; then y <=' b by Th49; hence [y,b] in BagOrder n by Def14; ::_thesis: verum end; A4: now__::_thesis:_for_y_being_Element_of_Bags_n_st_y_in_S_holds_ [(EmptyBag_n),y]_in_BagOrder_n let y be Element of Bags n; ::_thesis: ( y in S implies [(EmptyBag n),y] in BagOrder n ) assume y in S ; ::_thesis: [(EmptyBag n),y] in BagOrder n EmptyBag n <=' y by Th49, Th59; hence [(EmptyBag n),y] in BagOrder n by Def14; ::_thesis: verum end; A5: BagOrder n linearly_orders S by Lm4, ORDERS_1:38; EmptyBag n divides b by Th59; then EmptyBag n in S by A2; hence (divisors b) /. 1 = EmptyBag n by A1, A5, A4, Th20; ::_thesis: (divisors b) /. (len (divisors b)) = b b in S by A2; hence (divisors b) /. (len (divisors b)) = b by A1, A5, A3, Th21; ::_thesis: verum end; theorem Th66: :: PRE_POLY:66 for n being Ordinal for i being Nat for b, b1, b2 being bag of n st i > 1 & i < len (divisors b) holds ( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b ) proof let n be Ordinal; ::_thesis: for i being Nat for b, b1, b2 being bag of n st i > 1 & i < len (divisors b) holds ( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b ) let i be Nat; ::_thesis: for b, b1, b2 being bag of n st i > 1 & i < len (divisors b) holds ( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b ) let b, b1, b2 be bag of n; ::_thesis: ( i > 1 & i < len (divisors b) implies ( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b ) ) A1: ( 1 in dom (divisors b) & len (divisors b) in dom (divisors b) ) by FINSEQ_5:6; A2: ( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b ) by Th65; assume A3: ( i > 1 & i < len (divisors b) ) ; ::_thesis: ( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b ) then i in dom (divisors b) by FINSEQ_3:25; hence ( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b ) by A2, A1, A3, PARTFUN2:10; ::_thesis: verum end; theorem Th67: :: PRE_POLY:67 for n being Ordinal holds divisors (EmptyBag n) = <*(EmptyBag n)*> proof let n be Ordinal; ::_thesis: divisors (EmptyBag n) = <*(EmptyBag n)*> consider S being non empty finite Subset of (Bags n) such that A1: divisors (EmptyBag n) = SgmX ((BagOrder n),S) and A2: for p being bag of n holds ( p in S iff p divides EmptyBag n ) by Def16; A3: S c= {(EmptyBag n)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in {(EmptyBag n)} ) assume A4: x in S ; ::_thesis: x in {(EmptyBag n)} then reconsider b = x as bag of n ; b divides EmptyBag n by A2, A4; then b = EmptyBag n by Th58; hence x in {(EmptyBag n)} by TARSKI:def_1; ::_thesis: verum end; A5: BagOrder n linearly_orders S by Lm4, ORDERS_1:38; EmptyBag n in S by A2; then {(EmptyBag n)} c= S by ZFMISC_1:31; then S = {(EmptyBag n)} by A3, XBOOLE_0:def_10; then A6: rng (divisors (EmptyBag n)) = {(EmptyBag n)} by A1, A5, Def2; len (divisors (EmptyBag n)) = card (rng (divisors (EmptyBag n))) by Th19 .= 1 by A6, CARD_1:30 ; hence divisors (EmptyBag n) = <*(EmptyBag n)*> by A6, FINSEQ_1:39; ::_thesis: verum end; definition let n be Ordinal; let b be bag of n; func decomp b -> FinSequence of 2 -tuples_on (Bags n) means :Def17: :: PRE_POLY:def 17 ( dom it = dom (divisors b) & ( for i being Element of NAT for p being bag of n st i in dom it & p = (divisors b) /. i holds it /. i = <*p,(b -' p)*> ) ); existence ex b1 being FinSequence of 2 -tuples_on (Bags n) st ( dom b1 = dom (divisors b) & ( for i being Element of NAT for p being bag of n st i in dom b1 & p = (divisors b) /. i holds b1 /. i = <*p,(b -' p)*> ) ) proof defpred S1[ Nat, set ] means for p being bag of n st p = (divisors b) /. $1 holds $2 = <*p,(b -' p)*>; A1: for k being Nat st k in Seg (len (divisors b)) holds ex d being Element of 2 -tuples_on (Bags n) st S1[k,d] proof let k be Nat; ::_thesis: ( k in Seg (len (divisors b)) implies ex d being Element of 2 -tuples_on (Bags n) st S1[k,d] ) assume k in Seg (len (divisors b)) ; ::_thesis: ex d being Element of 2 -tuples_on (Bags n) st S1[k,d] reconsider p = (divisors b) /. k as bag of n ; reconsider b1 = p, b2 = b -' p as Element of Bags n by Def12; len <*p,(b -' p)*> = 2 by FINSEQ_1:44; then reconsider d = <*b1,b2*> as Element of 2 -tuples_on (Bags n) by FINSEQ_2:92; take d ; ::_thesis: S1[k,d] thus S1[k,d] ; ::_thesis: verum end; consider f being FinSequence of 2 -tuples_on (Bags n) such that A2: len f = len (divisors b) and A3: for n being Nat st n in Seg (len (divisors b)) holds S1[n,f /. n] from FINSEQ_4:sch_1(A1); take f ; ::_thesis: ( dom f = dom (divisors b) & ( for i being Element of NAT for p being bag of n st i in dom f & p = (divisors b) /. i holds f /. i = <*p,(b -' p)*> ) ) thus dom f = dom (divisors b) by A2, FINSEQ_3:29; ::_thesis: for i being Element of NAT for p being bag of n st i in dom f & p = (divisors b) /. i holds f /. i = <*p,(b -' p)*> let i be Element of NAT ; ::_thesis: for p being bag of n st i in dom f & p = (divisors b) /. i holds f /. i = <*p,(b -' p)*> let p be bag of n; ::_thesis: ( i in dom f & p = (divisors b) /. i implies f /. i = <*p,(b -' p)*> ) assume that A4: i in dom f and A5: p = (divisors b) /. i ; ::_thesis: f /. i = <*p,(b -' p)*> i in Seg (len (divisors b)) by A2, A4, FINSEQ_1:def_3; hence f /. i = <*p,(b -' p)*> by A3, A5; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of 2 -tuples_on (Bags n) st dom b1 = dom (divisors b) & ( for i being Element of NAT for p being bag of n st i in dom b1 & p = (divisors b) /. i holds b1 /. i = <*p,(b -' p)*> ) & dom b2 = dom (divisors b) & ( for i being Element of NAT for p being bag of n st i in dom b2 & p = (divisors b) /. i holds b2 /. i = <*p,(b -' p)*> ) holds b1 = b2 proof let F, G be FinSequence of 2 -tuples_on (Bags n); ::_thesis: ( dom F = dom (divisors b) & ( for i being Element of NAT for p being bag of n st i in dom F & p = (divisors b) /. i holds F /. i = <*p,(b -' p)*> ) & dom G = dom (divisors b) & ( for i being Element of NAT for p being bag of n st i in dom G & p = (divisors b) /. i holds G /. i = <*p,(b -' p)*> ) implies F = G ) assume that A6: dom F = dom (divisors b) and A7: for i being Element of NAT for p being bag of n st i in dom F & p = (divisors b) /. i holds F /. i = <*p,(b -' p)*> and A8: dom G = dom (divisors b) and A9: for i being Element of NAT for p being bag of n st i in dom G & p = (divisors b) /. i holds G /. i = <*p,(b -' p)*> ; ::_thesis: F = G now__::_thesis:_for_i_being_Nat_st_i_in_dom_F_holds_ F_/._i_=_G_/._i let i be Nat; ::_thesis: ( i in dom F implies F /. i = G /. i ) reconsider p = (divisors b) /. i as bag of n ; assume A10: i in dom F ; ::_thesis: F /. i = G /. i hence F /. i = <*p,(b -' p)*> by A7 .= G /. i by A6, A8, A9, A10 ; ::_thesis: verum end; hence F = G by A6, A8, FINSEQ_5:12; ::_thesis: verum end; end; :: deftheorem Def17 defines decomp PRE_POLY:def_17_:_ for n being Ordinal for b being bag of n for b3 being FinSequence of 2 -tuples_on (Bags n) holds ( b3 = decomp b iff ( dom b3 = dom (divisors b) & ( for i being Element of NAT for p being bag of n st i in dom b3 & p = (divisors b) /. i holds b3 /. i = <*p,(b -' p)*> ) ) ); theorem Th68: :: PRE_POLY:68 for n being Ordinal for i being Element of NAT for b being bag of n st i in dom (decomp b) holds ex b1, b2 being bag of n st ( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 ) proof let n be Ordinal; ::_thesis: for i being Element of NAT for b being bag of n st i in dom (decomp b) holds ex b1, b2 being bag of n st ( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 ) let i be Element of NAT ; ::_thesis: for b being bag of n st i in dom (decomp b) holds ex b1, b2 being bag of n st ( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 ) let b be bag of n; ::_thesis: ( i in dom (decomp b) implies ex b1, b2 being bag of n st ( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 ) ) reconsider p = (divisors b) /. i as bag of n ; assume A1: i in dom (decomp b) ; ::_thesis: ex b1, b2 being bag of n st ( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 ) take p ; ::_thesis: ex b2 being bag of n st ( (decomp b) /. i = <*p,b2*> & b = p + b2 ) take b -' p ; ::_thesis: ( (decomp b) /. i = <*p,(b -' p)*> & b = p + (b -' p) ) thus (decomp b) /. i = <*p,(b -' p)*> by A1, Def17; ::_thesis: b = p + (b -' p) i in dom (divisors b) by A1, Def17; hence b = p + (b -' p) by Th47, Th64; ::_thesis: verum end; theorem Th69: :: PRE_POLY:69 for n being Ordinal for b, b1, b2 being bag of n st b = b1 + b2 holds ex i being Element of NAT st ( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> ) proof let n be Ordinal; ::_thesis: for b, b1, b2 being bag of n st b = b1 + b2 holds ex i being Element of NAT st ( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> ) let b, b1, b2 be bag of n; ::_thesis: ( b = b1 + b2 implies ex i being Element of NAT st ( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> ) ) consider S being non empty finite Subset of (Bags n) such that A1: divisors b = SgmX ((BagOrder n),S) and A2: for p being bag of n holds ( p in S iff p divides b ) by Def16; A3: BagOrder n linearly_orders S by Lm4, ORDERS_1:38; assume A4: b = b1 + b2 ; ::_thesis: ex i being Element of NAT st ( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> ) then b1 divides b by Th50; then b1 in S by A2; then b1 in rng (divisors b) by A1, A3, Def2; then consider i being Element of NAT such that A5: i in dom (divisors b) and A6: (divisors b) /. i = b1 by PARTFUN2:2; take i ; ::_thesis: ( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> ) thus i in dom (decomp b) by A5, Def17; ::_thesis: (decomp b) /. i = <*b1,b2*> then (decomp b) /. i = <*b1,(b -' b1)*> by A6, Def17; hence (decomp b) /. i = <*b1,b2*> by A4, Th48; ::_thesis: verum end; theorem Th70: :: PRE_POLY:70 for n being Ordinal for i being Element of NAT for b, b1, b2 being bag of n st i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> holds b1 = (divisors b) /. i proof let n be Ordinal; ::_thesis: for i being Element of NAT for b, b1, b2 being bag of n st i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> holds b1 = (divisors b) /. i let i be Element of NAT ; ::_thesis: for b, b1, b2 being bag of n st i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> holds b1 = (divisors b) /. i let b, b1, b2 be bag of n; ::_thesis: ( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> implies b1 = (divisors b) /. i ) reconsider p = (divisors b) /. i as bag of n ; assume ( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> ) ; ::_thesis: b1 = (divisors b) /. i then <*b1,b2*> = <*p,(b -' p)*> by Def17; hence b1 = (divisors b) /. i by FINSEQ_1:77; ::_thesis: verum end; registration let n be Ordinal; let b be bag of n; cluster decomp b -> one-to-one non empty FinSequence-yielding ; coherence ( not decomp b is empty & decomp b is one-to-one & decomp b is FinSequence-yielding ) proof A1: dom (divisors b) = dom (decomp b) by Def17; hence not decomp b is empty ; ::_thesis: ( decomp b is one-to-one & decomp b is FinSequence-yielding ) now__::_thesis:_for_k,_m_being_Element_of_NAT_st_k_in_dom_(decomp_b)_&_m_in_dom_(decomp_b)_&_(decomp_b)_/._k_=_(decomp_b)_/._m_holds_ k_=_m let k, m be Element of NAT ; ::_thesis: ( k in dom (decomp b) & m in dom (decomp b) & (decomp b) /. k = (decomp b) /. m implies k = m ) assume A2: k in dom (decomp b) ; ::_thesis: ( m in dom (decomp b) & (decomp b) /. k = (decomp b) /. m implies k = m ) assume A3: m in dom (decomp b) ; ::_thesis: ( (decomp b) /. k = (decomp b) /. m implies k = m ) then consider bm1, bm2 being bag of n such that A4: (decomp b) /. m = <*bm1,bm2*> and b = bm1 + bm2 by Th68; assume (decomp b) /. k = (decomp b) /. m ; ::_thesis: k = m then (divisors b) /. k = bm1 by A2, A4, Th70 .= (divisors b) /. m by A3, A4, Th70 ; hence k = m by A1, A2, A3, PARTFUN2:10; ::_thesis: verum end; hence decomp b is one-to-one by PARTFUN2:9; ::_thesis: decomp b is FinSequence-yielding let x be set ; :: according to PRE_POLY:def_3 ::_thesis: ( x in dom (decomp b) implies (decomp b) . x is FinSequence ) assume x in dom (decomp b) ; ::_thesis: (decomp b) . x is FinSequence then reconsider k = x as Element of NAT ; reconsider p = (divisors b) /. k as bag of n ; thus (decomp b) . x is FinSequence ; ::_thesis: verum end; end; registration let n be Ordinal; let b be Element of Bags n; cluster decomp b -> one-to-one non empty FinSequence-yielding ; coherence ( not decomp b is empty & decomp b is one-to-one & decomp b is FinSequence-yielding ) ; end; theorem :: PRE_POLY:71 for n being Ordinal for b being bag of n holds ( (decomp b) /. 1 = <*(EmptyBag n),b*> & (decomp b) /. (len (decomp b)) = <*b,(EmptyBag n)*> ) proof let n be Ordinal; ::_thesis: for b being bag of n holds ( (decomp b) /. 1 = <*(EmptyBag n),b*> & (decomp b) /. (len (decomp b)) = <*b,(EmptyBag n)*> ) let b be bag of n; ::_thesis: ( (decomp b) /. 1 = <*(EmptyBag n),b*> & (decomp b) /. (len (decomp b)) = <*b,(EmptyBag n)*> ) reconsider p = (divisors b) /. 1 as bag of n ; ( p = EmptyBag n & 1 in dom (decomp b) ) by Th65, FINSEQ_5:6; hence (decomp b) /. 1 = <*(EmptyBag n),(b -' (EmptyBag n))*> by Def17 .= <*(EmptyBag n),b*> by Th54 ; ::_thesis: (decomp b) /. (len (decomp b)) = <*b,(EmptyBag n)*> reconsider p = (divisors b) /. (len (decomp b)) as bag of n ; dom (decomp b) = dom (divisors b) by Def17; then len (decomp b) = len (divisors b) by FINSEQ_3:29; then A1: p = b by Th65; len (decomp b) in dom (decomp b) by FINSEQ_5:6; hence (decomp b) /. (len (decomp b)) = <*b,(b -' b)*> by A1, Def17 .= <*b,(EmptyBag n)*> by Th56 ; ::_thesis: verum end; theorem :: PRE_POLY:72 for n being Ordinal for i being Nat for b, b1, b2 being bag of n st i > 1 & i < len (decomp b) & (decomp b) /. i = <*b1,b2*> holds ( b1 <> EmptyBag n & b2 <> EmptyBag n ) proof let n be Ordinal; ::_thesis: for i being Nat for b, b1, b2 being bag of n st i > 1 & i < len (decomp b) & (decomp b) /. i = <*b1,b2*> holds ( b1 <> EmptyBag n & b2 <> EmptyBag n ) let i be Nat; ::_thesis: for b, b1, b2 being bag of n st i > 1 & i < len (decomp b) & (decomp b) /. i = <*b1,b2*> holds ( b1 <> EmptyBag n & b2 <> EmptyBag n ) let b, b1, b2 be bag of n; ::_thesis: ( i > 1 & i < len (decomp b) & (decomp b) /. i = <*b1,b2*> implies ( b1 <> EmptyBag n & b2 <> EmptyBag n ) ) assume that A1: ( i > 1 & i < len (decomp b) ) and A2: (decomp b) /. i = <*b1,b2*> ; ::_thesis: ( b1 <> EmptyBag n & b2 <> EmptyBag n ) reconsider p = (divisors b) /. i as bag of n ; A3: i in dom (decomp b) by A1, FINSEQ_3:25; then A4: (decomp b) /. i = <*p,(b -' p)*> by Def17; then A5: b2 = b -' p by A2, FINSEQ_1:77; A6: dom (decomp b) = dom (divisors b) by Def17; then A7: len (decomp b) = len (divisors b) by FINSEQ_3:29; b1 = p by A2, A4, FINSEQ_1:77; hence b1 <> EmptyBag n by A1, A7, Th66; ::_thesis: b2 <> EmptyBag n assume b2 = EmptyBag n ; ::_thesis: contradiction then p = b by A6, A3, A5, Th57, Th64; hence contradiction by A1, A7, Th66; ::_thesis: verum end; theorem :: PRE_POLY:73 for n being Ordinal holds decomp (EmptyBag n) = <*<*(EmptyBag n),(EmptyBag n)*>*> proof let n be Ordinal; ::_thesis: decomp (EmptyBag n) = <*<*(EmptyBag n),(EmptyBag n)*>*> len <*(EmptyBag n),(EmptyBag n)*> = 2 by FINSEQ_1:44; then reconsider E = <*(EmptyBag n),(EmptyBag n)*> as Element of 2 -tuples_on (Bags n) by FINSEQ_2:92; reconsider e = <*E*> as FinSequence of 2 -tuples_on (Bags n) ; A1: dom e = Seg 1 by FINSEQ_1:38; A2: <*(EmptyBag n)*> = divisors (EmptyBag n) by Th67; A3: for i being Element of NAT for p being bag of n st i in dom e & p = (divisors (EmptyBag n)) /. i holds e /. i = <*p,((EmptyBag n) -' p)*> proof let i be Element of NAT ; ::_thesis: for p being bag of n st i in dom e & p = (divisors (EmptyBag n)) /. i holds e /. i = <*p,((EmptyBag n) -' p)*> let p be bag of n; ::_thesis: ( i in dom e & p = (divisors (EmptyBag n)) /. i implies e /. i = <*p,((EmptyBag n) -' p)*> ) assume that A4: i in dom e and A5: p = (divisors (EmptyBag n)) /. i ; ::_thesis: e /. i = <*p,((EmptyBag n) -' p)*> A6: i = 1 by A1, A4, FINSEQ_1:2, TARSKI:def_1; then A7: (divisors (EmptyBag n)) /. i = EmptyBag n by A2, FINSEQ_4:16; thus e /. i = E by A6, FINSEQ_4:16 .= <*p,((EmptyBag n) -' p)*> by A5, A7, Th54 ; ::_thesis: verum end; dom e = dom (divisors (EmptyBag n)) by A2, A1, FINSEQ_1:38; hence decomp (EmptyBag n) = <*<*(EmptyBag n),(EmptyBag n)*>*> by A3, Def17; ::_thesis: verum end; theorem :: PRE_POLY:74 for n being Ordinal for b being bag of n for f, g being FinSequence of (3 -tuples_on (Bags n)) * st dom f = dom (decomp b) & dom g = dom (decomp b) & ( for k being Nat st k in dom f holds f . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) ) & ( for k being Nat st k in dom g holds g . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) ) holds ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p proof let n be Ordinal; ::_thesis: for b being bag of n for f, g being FinSequence of (3 -tuples_on (Bags n)) * st dom f = dom (decomp b) & dom g = dom (decomp b) & ( for k being Nat st k in dom f holds f . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) ) & ( for k being Nat st k in dom g holds g . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) ) holds ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p let b be bag of n; ::_thesis: for f, g being FinSequence of (3 -tuples_on (Bags n)) * st dom f = dom (decomp b) & dom g = dom (decomp b) & ( for k being Nat st k in dom f holds f . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) ) & ( for k being Nat st k in dom g holds g . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) ) holds ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p let f, g be FinSequence of (3 -tuples_on (Bags n)) * ; ::_thesis: ( dom f = dom (decomp b) & dom g = dom (decomp b) & ( for k being Nat st k in dom f holds f . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) ) & ( for k being Nat st k in dom g holds g . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) ) implies ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p ) assume that A1: dom f = dom (decomp b) and A2: dom g = dom (decomp b) and A3: for k being Nat st k in dom f holds f . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) and A4: for k being Nat st k in dom g holds g . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) ; ::_thesis: ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p set Ff = FlattenSeq f; set Fg = FlattenSeq g; set db = decomp b; A5: FlattenSeq g is one-to-one proof let k1, k2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not k1 in dom (FlattenSeq g) or not k2 in dom (FlattenSeq g) or not (FlattenSeq g) . k1 = (FlattenSeq g) . k2 or k1 = k2 ) assume that A6: k1 in dom (FlattenSeq g) and A7: k2 in dom (FlattenSeq g) and A8: (FlattenSeq g) . k1 = (FlattenSeq g) . k2 ; ::_thesis: k1 = k2 consider i1, j1 being Element of NAT such that A9: i1 in dom g and A10: j1 in dom (g . i1) and A11: k1 = (Sum (Card (g | (i1 -' 1)))) + j1 and A12: (g . i1) . j1 = (FlattenSeq g) . k1 by A6, Th29; reconsider dbi1 = (decomp b) /. i1 as Element of 2 -tuples_on (Bags n) ; set ddbi11 = decomp (dbi1 /. 2); A13: g . i1 = ((len (decomp (dbi1 /. 2))) |-> <*(dbi1 /. 1)*>) ^^ (decomp (dbi1 /. 2)) by A4, A9; then A14: dom (g . i1) = (dom (decomp (dbi1 /. 2))) /\ (dom ((len (decomp (dbi1 /. 2))) |-> <*(dbi1 /. 1)*>)) by Def4 .= (dom (decomp (dbi1 /. 2))) /\ (Seg (len (decomp (dbi1 /. 2)))) by FUNCOP_1:13 .= (dom (decomp (dbi1 /. 2))) /\ (dom (decomp (dbi1 /. 2))) by FINSEQ_1:def_3 .= dom (decomp (dbi1 /. 2)) ; then A15: (decomp (dbi1 /. 2)) /. j1 = (decomp (dbi1 /. 2)) . j1 by A10, PARTFUN1:def_6; dom (decomp (dbi1 /. 2)) = Seg (len (decomp (dbi1 /. 2))) by FINSEQ_1:def_3; then A16: ((len (decomp (dbi1 /. 2))) |-> <*(dbi1 /. 1)*>) . j1 = <*(dbi1 /. 1)*> by A10, A14, FUNCOP_1:7; consider b11, b12 being bag of n such that A17: (decomp b) /. i1 = <*b11,b12*> and b = b11 + b12 by A2, A9, Th68; reconsider b119 = b11, b129 = b12 as Element of Bags n by Def12; A18: ( b119 = b11 & b129 = b12 ) ; then dbi1 /. 2 = b12 by A17, FINSEQ_4:17; then consider b111, b112 being bag of n such that A19: (decomp (dbi1 /. 2)) /. j1 = <*b111,b112*> and A20: b12 = b111 + b112 by A10, A14, Th68; dbi1 /. 1 = b11 by A17, A18, FINSEQ_4:17; then A21: (g . i1) . j1 = <*b11*> ^ <*b111,b112*> by A10, A13, A19, A15, A16, Def4 .= <*b11,b111,b112*> by FINSEQ_1:43 ; consider i2, j2 being Element of NAT such that A22: i2 in dom g and A23: j2 in dom (g . i2) and A24: k2 = (Sum (Card (g | (i2 -' 1)))) + j2 and A25: (g . i2) . j2 = (FlattenSeq g) . k2 by A7, Th29; reconsider dbi2 = (decomp b) /. i2 as Element of 2 -tuples_on (Bags n) ; set ddbi21 = decomp (dbi2 /. 2); A26: g . i2 = ((len (decomp (dbi2 /. 2))) |-> <*(dbi2 /. 1)*>) ^^ (decomp (dbi2 /. 2)) by A4, A22; then A27: dom (g . i2) = (dom (decomp (dbi2 /. 2))) /\ (dom ((len (decomp (dbi2 /. 2))) |-> <*(dbi2 /. 1)*>)) by Def4 .= (dom (decomp (dbi2 /. 2))) /\ (Seg (len (decomp (dbi2 /. 2)))) by FUNCOP_1:13 .= (dom (decomp (dbi2 /. 2))) /\ (dom (decomp (dbi2 /. 2))) by FINSEQ_1:def_3 .= dom (decomp (dbi2 /. 2)) ; then A28: (decomp (dbi2 /. 2)) /. j2 = (decomp (dbi2 /. 2)) . j2 by A23, PARTFUN1:def_6; dom (decomp (dbi2 /. 2)) = Seg (len (decomp (dbi2 /. 2))) by FINSEQ_1:def_3; then A29: ((len (decomp (dbi2 /. 2))) |-> <*(dbi2 /. 1)*>) . j2 = <*(dbi2 /. 1)*> by A23, A27, FUNCOP_1:7; consider b21, b22 being bag of n such that A30: (decomp b) /. i2 = <*b21,b22*> and b = b21 + b22 by A2, A22, Th68; reconsider b219 = b21, b229 = b22 as Element of Bags n by Def12; A31: ( b219 = b21 & b229 = b22 ) ; then dbi2 /. 2 = b22 by A30, FINSEQ_4:17; then consider b211, b212 being bag of n such that A32: (decomp (dbi2 /. 2)) /. j2 = <*b211,b212*> and A33: b22 = b211 + b212 by A23, A27, Th68; dbi2 /. 1 = b21 by A30, A31, FINSEQ_4:17; then A34: (g . i2) . j2 = <*b21*> ^ <*b211,b212*> by A23, A26, A32, A28, A29, Def4 .= <*b21,b211,b212*> by FINSEQ_1:43 ; then A35: ( b111 = b211 & b112 = b212 ) by A8, A12, A25, A21, FINSEQ_1:78; A36: (decomp b) /. i2 = (decomp b) . i2 by A2, A22, PARTFUN1:def_6; A37: (decomp b) /. i1 = (decomp b) . i1 by A2, A9, PARTFUN1:def_6; b11 = b21 by A8, A12, A25, A21, A34, FINSEQ_1:78; then i1 = i2 by A2, A9, A22, A37, A17, A20, A36, A30, A33, A35, FUNCT_1:def_4; hence k1 = k2 by A10, A11, A23, A24, A19, A15, A27, A32, A28, A35, FUNCT_1:def_4; ::_thesis: verum end; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_rng_(FlattenSeq_f)_implies_y_in_rng_(FlattenSeq_g)_)_&_(_y_in_rng_(FlattenSeq_g)_implies_y_in_rng_(FlattenSeq_f)_)_) let y be set ; ::_thesis: ( ( y in rng (FlattenSeq f) implies y in rng (FlattenSeq g) ) & ( y in rng (FlattenSeq g) implies y in rng (FlattenSeq f) ) ) hereby ::_thesis: ( y in rng (FlattenSeq g) implies y in rng (FlattenSeq f) ) assume y in rng (FlattenSeq f) ; ::_thesis: y in rng (FlattenSeq g) then consider k being set such that A38: k in dom (FlattenSeq f) and A39: y = (FlattenSeq f) . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A38; consider i, j being Element of NAT such that A40: i in dom f and A41: j in dom (f . i) and k = (Sum (Card (f | (i -' 1)))) + j and A42: (f . i) . j = (FlattenSeq f) . k by A38, Th29; reconsider dbi = (decomp b) /. i as Element of 2 -tuples_on (Bags n) ; set ddbi1 = decomp (dbi /. 1); A43: f . i = (decomp (dbi /. 1)) ^^ ((len (decomp (dbi /. 1))) |-> <*(dbi /. 2)*>) by A3, A40; then A44: dom (f . i) = (dom (decomp (dbi /. 1))) /\ (dom ((len (decomp (dbi /. 1))) |-> <*(dbi /. 2)*>)) by Def4 .= (dom (decomp (dbi /. 1))) /\ (Seg (len (decomp (dbi /. 1)))) by FUNCOP_1:13 .= (dom (decomp (dbi /. 1))) /\ (dom (decomp (dbi /. 1))) by FINSEQ_1:def_3 .= dom (decomp (dbi /. 1)) ; dom (decomp (dbi /. 1)) = Seg (len (decomp (dbi /. 1))) by FINSEQ_1:def_3; then A45: ((len (decomp (dbi /. 1))) |-> <*(dbi /. 2)*>) . j = <*(dbi /. 2)*> by A41, A44, FUNCOP_1:7; consider b1, b2 being bag of n such that A46: (decomp b) /. i = <*b1,b2*> and A47: b = b1 + b2 by A1, A40, Th68; reconsider b19 = b1, b29 = b2 as Element of Bags n by Def12; A48: ( b19 = b1 & b29 = b2 ) ; then A49: dbi /. 2 = b2 by A46, FINSEQ_4:17; dbi /. 1 = b1 by A46, A48, FINSEQ_4:17; then consider b11, b12 being bag of n such that A50: (decomp (dbi /. 1)) /. j = <*b11,b12*> and A51: b1 = b11 + b12 by A41, A44, Th68; b = b11 + (b12 + b2) by A47, A51, Th35; then consider i9 being Element of NAT such that A52: i9 in dom (decomp b) and A53: (decomp b) /. i9 = <*b11,(b12 + b2)*> by Th69; set b3 = b12 + b2; reconsider b119 = b11, b39 = b12 + b2 as Element of Bags n by Def12; consider j9 being Element of NAT such that A54: j9 in dom (decomp (b12 + b2)) and A55: (decomp (b12 + b2)) /. j9 = <*b12,b2*> by Th69; reconsider dbi9 = (decomp b) /. i9 as Element of 2 -tuples_on (Bags n) ; set ddbi92 = decomp (dbi9 /. 2); A56: (decomp b) /. i9 = <*b119,b39*> by A53; then A57: ( dbi9 /. 1 = b11 & decomp (dbi9 /. 2) = decomp (b12 + b2) ) by FINSEQ_4:17; A58: g . i9 = ((len (decomp (dbi9 /. 2))) |-> <*(dbi9 /. 1)*>) ^^ (decomp (dbi9 /. 2)) by A2, A4, A52; then A59: dom (g . i9) = (dom ((len (decomp (dbi9 /. 2))) |-> <*(dbi9 /. 1)*>)) /\ (dom (decomp (dbi9 /. 2))) by Def4 .= (Seg (len (decomp (dbi9 /. 2)))) /\ (dom (decomp (dbi9 /. 2))) by FUNCOP_1:13 .= (dom (decomp (dbi9 /. 2))) /\ (dom (decomp (dbi9 /. 2))) by FINSEQ_1:def_3 .= dom (decomp (dbi9 /. 2)) ; then A60: j9 in dom (g . i9) by A54, A56, FINSEQ_4:17; then A61: j9 in Seg (len (decomp (dbi9 /. 2))) by A59, FINSEQ_1:def_3; A62: (decomp (b12 + b2)) /. j9 = (decomp (b12 + b2)) . j9 by A54, PARTFUN1:def_6; set m = (Sum (Card (g | (i9 -' 1)))) + j9; A63: ( (Sum (Card (g | (i9 -' 1)))) + j9 in dom (FlattenSeq g) & (FlattenSeq g) . ((Sum (Card (g | (i9 -' 1)))) + j9) = (g . i9) . j9 ) by A2, A52, A60, Th30; A64: (g . i9) . j9 = (((len (decomp (dbi9 /. 2))) |-> <*(dbi9 /. 1)*>) . j9) ^ ((decomp (dbi9 /. 2)) . j9) by A58, A60, Def4 .= <*b11*> ^ <*b12,b2*> by A55, A57, A61, A62, FUNCOP_1:7 .= <*b11,b12,b2*> by FINSEQ_1:43 ; (decomp (dbi /. 1)) /. j = (decomp (dbi /. 1)) . j by A41, A44, PARTFUN1:def_6; then (f . i) . j = <*b11,b12*> ^ <*b2*> by A41, A43, A49, A50, A45, Def4 .= <*b11,b12,b2*> by FINSEQ_1:43 ; hence y in rng (FlattenSeq g) by A39, A42, A64, A63, FUNCT_1:def_3; ::_thesis: verum end; assume y in rng (FlattenSeq g) ; ::_thesis: y in rng (FlattenSeq f) then consider k being set such that A65: k in dom (FlattenSeq g) and A66: y = (FlattenSeq g) . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A65; consider i, j being Element of NAT such that A67: i in dom g and A68: j in dom (g . i) and k = (Sum (Card (g | (i -' 1)))) + j and A69: (g . i) . j = (FlattenSeq g) . k by A65, Th29; reconsider dbi = (decomp b) /. i as Element of 2 -tuples_on (Bags n) ; set ddbi1 = decomp (dbi /. 2); A70: g . i = ((len (decomp (dbi /. 2))) |-> <*(dbi /. 1)*>) ^^ (decomp (dbi /. 2)) by A4, A67; then A71: dom (g . i) = (dom (decomp (dbi /. 2))) /\ (dom ((len (decomp (dbi /. 2))) |-> <*(dbi /. 1)*>)) by Def4 .= (dom (decomp (dbi /. 2))) /\ (Seg (len (decomp (dbi /. 2)))) by FUNCOP_1:13 .= (dom (decomp (dbi /. 2))) /\ (dom (decomp (dbi /. 2))) by FINSEQ_1:def_3 .= dom (decomp (dbi /. 2)) ; dom (decomp (dbi /. 2)) = Seg (len (decomp (dbi /. 2))) by FINSEQ_1:def_3; then A72: ((len (decomp (dbi /. 2))) |-> <*(dbi /. 1)*>) . j = <*(dbi /. 1)*> by A68, A71, FUNCOP_1:7; consider b1, b2 being bag of n such that A73: (decomp b) /. i = <*b1,b2*> and A74: b = b1 + b2 by A2, A67, Th68; reconsider b19 = b1, b29 = b2 as Element of Bags n by Def12; A75: ( b19 = b1 & b29 = b2 ) ; then A76: dbi /. 1 = b1 by A73, FINSEQ_4:17; dbi /. 2 = b2 by A73, A75, FINSEQ_4:17; then consider b11, b12 being bag of n such that A77: (decomp (dbi /. 2)) /. j = <*b11,b12*> and A78: b2 = b11 + b12 by A68, A71, Th68; (decomp (dbi /. 2)) /. j = (decomp (dbi /. 2)) . j by A68, A71, PARTFUN1:def_6; then A79: (g . i) . j = <*b1*> ^ <*b11,b12*> by A68, A70, A76, A77, A72, Def4 .= <*b1,b11,b12*> by FINSEQ_1:43 ; set b3 = b1 + b11; reconsider b39 = b1 + b11, b129 = b12 as Element of Bags n by Def12; consider j9 being Element of NAT such that A80: j9 in dom (decomp (b1 + b11)) and A81: (decomp (b1 + b11)) /. j9 = <*b1,b11*> by Th69; A82: (decomp (b1 + b11)) /. j9 = (decomp (b1 + b11)) . j9 by A80, PARTFUN1:def_6; b = (b1 + b11) + b12 by A74, A78, Th35; then consider i9 being Element of NAT such that A83: i9 in dom (decomp b) and A84: (decomp b) /. i9 = <*(b1 + b11),b12*> by Th69; reconsider dbi9 = (decomp b) /. i9 as Element of 2 -tuples_on (Bags n) ; set ddbi92 = decomp (dbi9 /. 1); set m = (Sum (Card (f | (i9 -' 1)))) + j9; A85: (decomp b) /. i9 = <*b39,b129*> by A84; then A86: dbi9 /. 1 = b1 + b11 by FINSEQ_4:17; then A87: j9 in Seg (len (decomp (dbi9 /. 1))) by A80, FINSEQ_1:def_3; A88: f . i9 = (decomp (dbi9 /. 1)) ^^ ((len (decomp (dbi9 /. 1))) |-> <*(dbi9 /. 2)*>) by A1, A3, A83; then A89: dom (f . i9) = (dom ((len (decomp (dbi9 /. 1))) |-> <*(dbi9 /. 2)*>)) /\ (dom (decomp (dbi9 /. 1))) by Def4 .= (Seg (len (decomp (dbi9 /. 1)))) /\ (dom (decomp (dbi9 /. 1))) by FUNCOP_1:13 .= (dom (decomp (dbi9 /. 1))) /\ (dom (decomp (dbi9 /. 1))) by FINSEQ_1:def_3 .= dom (decomp (dbi9 /. 1)) ; then A90: ( (Sum (Card (f | (i9 -' 1)))) + j9 in dom (FlattenSeq f) & (FlattenSeq f) . ((Sum (Card (f | (i9 -' 1)))) + j9) = (f . i9) . j9 ) by A1, A83, A80, A86, Th30; A91: dbi9 /. 2 = b12 by A85, FINSEQ_4:17; (f . i9) . j9 = ((decomp (dbi9 /. 1)) . j9) ^ (((len (decomp (dbi9 /. 1))) |-> <*(dbi9 /. 2)*>) . j9) by A80, A88, A86, A89, Def4 .= <*b1,b11*> ^ <*b12*> by A81, A91, A86, A87, A82, FUNCOP_1:7 .= <*b1,b11,b12*> by FINSEQ_1:43 ; hence y in rng (FlattenSeq f) by A66, A69, A79, A90, FUNCT_1:def_3; ::_thesis: verum end; then A92: rng (FlattenSeq f) = rng (FlattenSeq g) by TARSKI:1; FlattenSeq f is one-to-one proof let k1, k2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not k1 in dom (FlattenSeq f) or not k2 in dom (FlattenSeq f) or not (FlattenSeq f) . k1 = (FlattenSeq f) . k2 or k1 = k2 ) assume that A93: k1 in dom (FlattenSeq f) and A94: k2 in dom (FlattenSeq f) and A95: (FlattenSeq f) . k1 = (FlattenSeq f) . k2 ; ::_thesis: k1 = k2 consider i1, j1 being Element of NAT such that A96: i1 in dom f and A97: j1 in dom (f . i1) and A98: k1 = (Sum (Card (f | (i1 -' 1)))) + j1 and A99: (f . i1) . j1 = (FlattenSeq f) . k1 by A93, Th29; reconsider dbi1 = (decomp b) /. i1 as Element of 2 -tuples_on (Bags n) ; set ddbi11 = decomp (dbi1 /. 1); A100: f . i1 = (decomp (dbi1 /. 1)) ^^ ((len (decomp (dbi1 /. 1))) |-> <*(dbi1 /. 2)*>) by A3, A96; then A101: dom (f . i1) = (dom (decomp (dbi1 /. 1))) /\ (dom ((len (decomp (dbi1 /. 1))) |-> <*(dbi1 /. 2)*>)) by Def4 .= (dom (decomp (dbi1 /. 1))) /\ (Seg (len (decomp (dbi1 /. 1)))) by FUNCOP_1:13 .= (dom (decomp (dbi1 /. 1))) /\ (dom (decomp (dbi1 /. 1))) by FINSEQ_1:def_3 .= dom (decomp (dbi1 /. 1)) ; then A102: (decomp (dbi1 /. 1)) /. j1 = (decomp (dbi1 /. 1)) . j1 by A97, PARTFUN1:def_6; dom (decomp (dbi1 /. 1)) = Seg (len (decomp (dbi1 /. 1))) by FINSEQ_1:def_3; then A103: ((len (decomp (dbi1 /. 1))) |-> <*(dbi1 /. 2)*>) . j1 = <*(dbi1 /. 2)*> by A97, A101, FUNCOP_1:7; consider b11, b12 being bag of n such that A104: (decomp b) /. i1 = <*b11,b12*> and b = b11 + b12 by A1, A96, Th68; reconsider b119 = b11, b129 = b12 as Element of Bags n by Def12; A105: ( b119 = b11 & b129 = b12 ) ; then dbi1 /. 1 = b11 by A104, FINSEQ_4:17; then consider b111, b112 being bag of n such that A106: (decomp (dbi1 /. 1)) /. j1 = <*b111,b112*> and A107: b11 = b111 + b112 by A97, A101, Th68; dbi1 /. 2 = b12 by A104, A105, FINSEQ_4:17; then A108: (f . i1) . j1 = <*b111,b112*> ^ <*b12*> by A97, A100, A106, A102, A103, Def4 .= <*b111,b112,b12*> by FINSEQ_1:43 ; consider i2, j2 being Element of NAT such that A109: i2 in dom f and A110: j2 in dom (f . i2) and A111: k2 = (Sum (Card (f | (i2 -' 1)))) + j2 and A112: (f . i2) . j2 = (FlattenSeq f) . k2 by A94, Th29; reconsider dbi2 = (decomp b) /. i2 as Element of 2 -tuples_on (Bags n) ; set ddbi21 = decomp (dbi2 /. 1); A113: f . i2 = (decomp (dbi2 /. 1)) ^^ ((len (decomp (dbi2 /. 1))) |-> <*(dbi2 /. 2)*>) by A3, A109; then A114: dom (f . i2) = (dom (decomp (dbi2 /. 1))) /\ (dom ((len (decomp (dbi2 /. 1))) |-> <*(dbi2 /. 2)*>)) by Def4 .= (dom (decomp (dbi2 /. 1))) /\ (Seg (len (decomp (dbi2 /. 1)))) by FUNCOP_1:13 .= (dom (decomp (dbi2 /. 1))) /\ (dom (decomp (dbi2 /. 1))) by FINSEQ_1:def_3 .= dom (decomp (dbi2 /. 1)) ; then A115: (decomp (dbi2 /. 1)) /. j2 = (decomp (dbi2 /. 1)) . j2 by A110, PARTFUN1:def_6; dom (decomp (dbi2 /. 1)) = Seg (len (decomp (dbi2 /. 1))) by FINSEQ_1:def_3; then A116: ((len (decomp (dbi2 /. 1))) |-> <*(dbi2 /. 2)*>) . j2 = <*(dbi2 /. 2)*> by A110, A114, FUNCOP_1:7; consider b21, b22 being bag of n such that A117: (decomp b) /. i2 = <*b21,b22*> and b = b21 + b22 by A1, A109, Th68; reconsider b219 = b21, b229 = b22 as Element of Bags n by Def12; A118: ( b219 = b21 & b229 = b22 ) ; then dbi2 /. 1 = b21 by A117, FINSEQ_4:17; then consider b211, b212 being bag of n such that A119: (decomp (dbi2 /. 1)) /. j2 = <*b211,b212*> and A120: b21 = b211 + b212 by A110, A114, Th68; dbi2 /. 2 = b22 by A117, A118, FINSEQ_4:17; then A121: (f . i2) . j2 = <*b211,b212*> ^ <*b22*> by A110, A113, A119, A115, A116, Def4 .= <*b211,b212,b22*> by FINSEQ_1:43 ; then A122: ( b111 = b211 & b112 = b212 ) by A95, A99, A112, A108, FINSEQ_1:78; A123: (decomp b) /. i2 = (decomp b) . i2 by A1, A109, PARTFUN1:def_6; A124: (decomp b) /. i1 = (decomp b) . i1 by A1, A96, PARTFUN1:def_6; b12 = b22 by A95, A99, A112, A108, A121, FINSEQ_1:78; then i1 = i2 by A1, A96, A109, A124, A104, A107, A123, A117, A120, A122, FUNCT_1:def_4; hence k1 = k2 by A97, A98, A110, A111, A106, A102, A114, A119, A115, A122, FUNCT_1:def_4; ::_thesis: verum end; then FlattenSeq f, FlattenSeq g are_fiberwise_equipotent by A92, A5, RFINSEQ:26; hence ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p by RFINSEQ:4; ::_thesis: verum end; theorem :: PRE_POLY:75 for X being set for b1, b2 being real-valued ManySortedSet of X holds support (b1 + b2) c= (support b1) \/ (support b2) proof let X be set ; ::_thesis: for b1, b2 being real-valued ManySortedSet of X holds support (b1 + b2) c= (support b1) \/ (support b2) let b1, b2 be real-valued ManySortedSet of X; ::_thesis: support (b1 + b2) c= (support b1) \/ (support b2) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (b1 + b2) or x in (support b1) \/ (support b2) ) assume x in support (b1 + b2) ; ::_thesis: x in (support b1) \/ (support b2) then A1: (b1 + b2) . x <> 0 by Def7; assume A2: not x in (support b1) \/ (support b2) ; ::_thesis: contradiction then not x in support b1 by XBOOLE_0:def_3; then A3: b1 . x = 0 by Def7; not x in support b2 by A2, XBOOLE_0:def_3; then (b1 . x) + (b2 . x) = 0 by A3, Def7; hence contradiction by A1, Def5; ::_thesis: verum end; registration let D be non empty set ; let n be Element of NAT ; cluster -> FinSequence-yielding for FinSequence of n -tuples_on D; coherence for b1 being FinSequence of n -tuples_on D holds b1 is FinSequence-yielding proof let p be FinSequence of n -tuples_on D; ::_thesis: p is FinSequence-yielding let x be set ; :: according to PRE_POLY:def_3 ::_thesis: ( x in dom p implies p . x is FinSequence ) assume x in dom p ; ::_thesis: p . x is FinSequence then reconsider i = x as Element of NAT ; thus p . x is FinSequence ; ::_thesis: verum end; end; registration let k be Element of NAT ; let D be non empty set ; let M be FinSequence of k -tuples_on D; let x be set ; clusterM /. x -> Relation-like Function-like ; coherence ( M /. x is Function-like & M /. x is Relation-like ) ; end; registration let k be Element of NAT ; let D be non empty set ; let M be FinSequence of k -tuples_on D; let x be set ; clusterM /. x -> D -valued FinSequence-like ; coherence ( M /. x is D -valued & M /. x is FinSequence-like ) ; end;