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