let p be partition of b; :: thesis: ( p = OrderedPartition b implies p is ordered )
assume A0: p = OrderedPartition b ; :: thesis: p is ordered
consider F, G being Function of NAT,(Bags the carrier of R) such that
A1: ( F . 0 = b & G . 0 = EmptyBag the carrier of R & ( for i being Nat holds
( G . (i + 1) = (F . i) | { x where x is Element of R : x is_maximal_in support (F . i) } & F . (i + 1) = (F . i) -' (G . (i + 1)) ) ) & ex i being Nat st
( F . i = EmptyBag the carrier of R & p = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) ) by OP, A0;
consider i being Nat such that
A2: ( F . i = EmptyBag the carrier of R & p = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) by A1;
set I = the carrier of R;
dom G = NAT by FUNCT_2:def 1;
then ( dom p = Seg i & i in NAT ) by A2, RELAT_1:62, ORDINAL1:def 12;
then A3: len p = i by FINSEQ_1:def 3;
defpred S1[ Nat] means for x being Element of R st (F . R) . x > 0 holds
(F . R) . x = b . x;
A4: S1[ 0 ] by A1;
A5: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume A6: S1[j] ; :: thesis: S1[j + 1]
let x be Element of R; :: thesis: ( (F . (j + 1)) . x > 0 implies (F . (j + 1)) . x = b . x )
assume A7: (F . (j + 1)) . x > 0 ; :: thesis: (F . (j + 1)) . x = b . x
set S = { y where y is Element of R : y is_maximal_in support (F . j) } ;
( F . (j + 1) = (F . j) -' (G . (j + 1)) & G . (j + 1) = (F . j) | { y where y is Element of R : y is_maximal_in support (F . j) } ) by A1;
then A8: (F . (j + 1)) . x = ((F . j) . x) -' (((F . j) | { y where y is Element of R : y is_maximal_in support (F . j) } ) . x) by PRE_POLY:def 6;
per cases ( x in { y where y is Element of R : y is_maximal_in support (F . j) } or not x in { y where y is Element of R : y is_maximal_in support (F . j) } ) ;
suppose x in { y where y is Element of R : y is_maximal_in support (F . j) } ; :: thesis: (F . (j + 1)) . x = b . x
then ((F . j) | { y where y is Element of R : y is_maximal_in support (F . j) } ) . x = (F . j) . x by BAR;
hence (F . (j + 1)) . x = b . x by A7, A8, XREAL_1:232; :: thesis: verum
end;
suppose not x in { y where y is Element of R : y is_maximal_in support (F . j) } ; :: thesis: (F . (j + 1)) . x = b . x
then ((F . j) | { y where y is Element of R : y is_maximal_in support (F . j) } ) . x = 0 by BAR;
then (F . (j + 1)) . x = (F . j) . x by A8, NAT_D:40;
hence (F . (j + 1)) . x = b . x by A6, A7; :: thesis: verum
end;
end;
end;
A9: for j being Nat holds S1[j] from NAT_1:sch 2(A4, A5);
hereby :: according to BAGORD_2:def 10 :: thesis: ( ( for m being bag of the carrier of R st m in rng p holds
for x, y being Element of R st m . x > 0 & m . y > 0 & x <> y holds
x ## y ) & ( for m being bag of the carrier of R st m in rng p holds
m <> EmptyBag the carrier of R ) & ( for i being Nat st i in dom p & i + 1 in dom p holds
for x being Element of R st (p /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (p /. i) . y > 0 & x <= y ) ) )
let a be bag of the carrier of R; :: thesis: ( a in rng p implies for x being Element of R st a . x > 0 holds
a . x = b . x )
assume a in rng p ; :: thesis: for x being Element of R st a . x > 0 holds
a . x = b . x
then consider j being object such that
B1: ( j in dom p & a = p . j ) by FUNCT_1:def 3;
reconsider j = j as Nat by B1;
consider k being Nat such that
B2: j = 1 + k by B1, FINSEQ_3:25, NAT_1:10;
set S = { x where x is Element of R : x is_maximal_in support (F . k) } ;
B3: ( a = G . j & G . j = (F . k) | { x where x is Element of R : x is_maximal_in support (F . k) } ) by A1, B2, B1, FUNCT_1:47;
let x be Element of R; :: thesis: ( a . x > 0 implies a . x = b . x )
assume B4: a . x > 0 ; :: thesis: a . x = b . x
then x in { x where x is Element of R : x is_maximal_in support (F . k) } by B3, BAR;
then a . x = (F . k) . x by B3, BAR;
hence a . x = b . x by A9, B4; :: thesis: verum
end;
hereby :: thesis: ( ( for m being bag of the carrier of R st m in rng p holds
m <> EmptyBag the carrier of R ) & ( for i being Nat st i in dom p & i + 1 in dom p holds
for x being Element of R st (p /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (p /. i) . y > 0 & x <= y ) ) )
let a be bag of the carrier of R; :: thesis: ( a in rng p implies for x, y being Element of R st a . x > 0 & a . y > 0 & x <> y holds
x ## y )
assume a in rng p ; :: thesis: for x, y being Element of R st a . x > 0 & a . y > 0 & x <> y holds
x ## y
then consider j being object such that
B1: ( j in dom p & a = p . j ) by FUNCT_1:def 3;
reconsider j = j as Nat by B1;
consider k being Nat such that
B2: j = 1 + k by B1, FINSEQ_3:25, NAT_1:10;
B3: ( a = G . j & G . j = (F . k) | { x where x is Element of R : x is_maximal_in support (F . k) } ) by A1, B2, B1, FUNCT_1:47;
{ x where x is Element of R : x is_maximal_in support (F . k) } c= support (F . k)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { x where x is Element of R : x is_maximal_in support (F . k) } or z in support (F . k) )
assume z in { x where x is Element of R : x is_maximal_in support (F . k) } ; :: thesis: z in support (F . k)
then ex x being Element of R st
( z = x & x is_maximal_in support (F . k) ) ;
hence z in support (F . k) by WAYBEL_4:55; :: thesis: verum
end;
then (support (F . k)) /\ { x where x is Element of R : x is_maximal_in support (F . k) } = { y where y is Element of R : y is_maximal_in support (F . k) } by XBOOLE_1:28;
then B4: support a = { x where x is Element of R : x is_maximal_in support (F . k) } by B3, Th44;
let x, y be Element of R; :: thesis: ( a . x > 0 & a . y > 0 & x <> y implies x ## y )
assume B5: ( a . x > 0 & a . y > 0 & x <> y ) ; :: thesis: x ## y
then x in support a by PRE_POLY:def 7;
then consider z being Element of R such that
B6: ( x = z & z is_maximal_in support (F . k) ) by B4;
y in support a by B5, PRE_POLY:def 7;
then consider u being Element of R such that
B7: ( y = u & u is_maximal_in support (F . k) ) by B4;
( x in support (F . k) & y in support (F . k) ) by B6, B7, WAYBEL_4:55;
then ( not x < y & not y < x ) by B6, B7, WAYBEL_4:55;
hence x ## y by Lem2; :: thesis: verum
end;
hereby :: thesis: for i being Nat st i in dom p & i + 1 in dom p holds
for x being Element of R st (p /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (p /. i) . y > 0 & x <= y )
let a be bag of the carrier of R; :: thesis: ( a in rng p implies a <> EmptyBag the carrier of R )
assume a in rng p ; :: thesis: a <> EmptyBag the carrier of R
then consider j being object such that
B1: ( j in dom p & a = p . j ) by FUNCT_1:def 3;
reconsider j = j as Nat by B1;
consider k being Nat such that
B2: j = 1 + k by B1, FINSEQ_3:25, NAT_1:10;
B3: ( a = G . j & G . j = (F . k) | { x where x is Element of R : x is_maximal_in support (F . k) } ) by A1, B2, B1, FUNCT_1:47;
( k < j & j <= i ) by A3, B2, B1, NAT_1:13, FINSEQ_3:25;
then k < i by XXREAL_0:2;
then B4: { x where x is Element of R : x is_maximal_in support (F . k) } <> {} by A2, Th42;
{ x where x is Element of R : x is_maximal_in support (F . k) } c= support (F . k)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { x where x is Element of R : x is_maximal_in support (F . k) } or z in support (F . k) )
assume z in { x where x is Element of R : x is_maximal_in support (F . k) } ; :: thesis: z in support (F . k)
then ex x being Element of R st
( z = x & x is_maximal_in support (F . k) ) ;
hence z in support (F . k) by WAYBEL_4:55; :: thesis: verum
end;
then (support (F . k)) /\ { x where x is Element of R : x is_maximal_in support (F . k) } = { y where y is Element of R : y is_maximal_in support (F . k) } by XBOOLE_1:28;
then support a = { x where x is Element of R : x is_maximal_in support (F . k) } by B3, Th44;
hence a <> EmptyBag the carrier of R by B4; :: thesis: verum
end;
let j be Nat; :: thesis: ( j in dom p & j + 1 in dom p implies for x being Element of R st (p /. (j + 1)) . x > 0 holds
ex y being Element of R st
( (p /. j) . y > 0 & x <= y ) )
assume C1: ( j in dom p & j + 1 in dom p ) ; :: thesis: for x being Element of R st (p /. (j + 1)) . x > 0 holds
ex y being Element of R st
( (p /. j) . y > 0 & x <= y )
then consider k being Nat such that
B2: j = 1 + k by NAT_1:10, FINSEQ_3:25;
let x be Element of R; :: thesis: ( (p /. (j + 1)) . x > 0 implies ex y being Element of R st
( (p /. j) . y > 0 & x <= y ) )
assume C2: (p /. (j + 1)) . x > 0 ; :: thesis: ex y being Element of R st
( (p /. j) . y > 0 & x <= y )
set S = { y where y is Element of R : y is_maximal_in support (F . j) } ;
set T = { y where y is Element of R : y is_maximal_in support (F . k) } ;
C4: ( p /. (j + 1) = p . (j + 1) & p . (j + 1) = G . (j + 1) & G . (j + 1) = (F . j) | { y where y is Element of R : y is_maximal_in support (F . j) } & p /. j = p . j & p . j = G . j & G . j = (F . k) | { y where y is Element of R : y is_maximal_in support (F . k) } & F . j = (F . k) -' (G . j) ) by C1, B2, A1, FUNCT_1:47, PARTFUN1:def 6;
then x in { y where y is Element of R : y is_maximal_in support (F . j) } by C2, BAR;
then consider y being Element of R such that
C5: ( x = y & y is_maximal_in support (F . j) ) ;
C6: ( x in support (F . j) & support (F . j) c= support (F . k) ) by C4, C5, WAYBEL_4:55, PRE_POLY:39;
{ y where y is Element of R : y is_maximal_in support (F . k) } c= support (F . k)
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { y where y is Element of R : y is_maximal_in support (F . k) } or u in support (F . k) )
assume u in { y where y is Element of R : y is_maximal_in support (F . k) } ; :: thesis: u in support (F . k)
then ex z being Element of R st
( u = z & z is_maximal_in support (F . k) ) ;
hence u in support (F . k) by WAYBEL_4:55; :: thesis: verum
end;
then (support (F . k)) /\ { y where y is Element of R : y is_maximal_in support (F . k) } = { y where y is Element of R : y is_maximal_in support (F . k) } by XBOOLE_1:28;
then D2: support (p /. j) = { y where y is Element of R : y is_maximal_in support (F . k) } by C4, Th44;
support (F . j) = (support (F . k)) \ { y where y is Element of R : y is_maximal_in support (F . k) } by C4, Th27A;
then not x in { y where y is Element of R : y is_maximal_in support (F . k) } by C6, XBOOLE_0:def 5;
then not x is_maximal_in support (F . k) ;
then consider z being Element of R such that
C7: ( z in support (F . k) & x < z ) by C6, WAYBEL_4:55;
take z ; :: thesis: ( (p /. j) . z > 0 & x <= z )
( not z in support (F . j) & support (F . j) = (support (F . k)) \ { y where y is Element of R : y is_maximal_in support (F . k) } ) by C4, C5, C7, Th27A, WAYBEL_4:55;
then z in { y where y is Element of R : y is_maximal_in support (F . k) } by C7, XBOOLE_0:def 5;
then (p /. j) . z <> 0 by D2, PRE_POLY:def 7;
hence (p /. j) . z > 0 ; :: thesis: x <= z
thus x <= z by C7, Lem2; :: thesis: verum