let n be Ordinal; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L holds BagOrder n linearly_orders Support p
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of n,L holds BagOrder n linearly_orders Support p
let p be Polynomial of n,L; :: thesis: BagOrder n linearly_orders Support p
set R = BagOrder n;
BagOrder n is connected by ORDERS_1:def 6;
then A1: BagOrder n is_connected_in field (BagOrder n) by RELAT_2:def 14;
for x being object st x in Bags n holds
x in field (BagOrder n)
proof
let x be object ; :: thesis: ( x in Bags n implies x in field (BagOrder n) )
assume x in Bags n ; :: thesis: x in field (BagOrder n)
then reconsider x = x as bag of n ;
EmptyBag n <=' x by PRE_POLY:60;
then [(EmptyBag n),x] in BagOrder n by PRE_POLY:def 14;
then A2: x in rng (BagOrder n) by XTUPLE_0:def 13;
field (BagOrder n) = (dom (BagOrder n)) \/ (rng (BagOrder n)) by RELAT_1:def 6;
then rng (BagOrder n) c= field (BagOrder n) by XBOOLE_1:7;
hence x in field (BagOrder n) by A2; :: thesis: verum
end;
then A3: Bags n c= field (BagOrder n) by TARSKI:def 3;
then [:(Bags n),(Bags n):] c= [:(field (BagOrder n)),(field (BagOrder n)):] by ZFMISC_1:96;
then reconsider R9 = BagOrder n as Relation of (field (BagOrder n)) by XBOOLE_1:1;
BagOrder n is_reflexive_in field (BagOrder n) by RELAT_2:def 9;
then dom R9 = field (BagOrder n) by ORDERS_1:13;
then A4: R9 is total by PARTFUN1:def 2;
Support p c= field (BagOrder n) by A3, XBOOLE_1:1;
then A5: R9 is_connected_in Support p by A1, A4, Lm2;
A6: BagOrder n is_antisymmetric_in Support p by Lm1;
A7: BagOrder n is_transitive_in Support p by Lm1;
BagOrder n is_reflexive_in Support p by Lm1;
hence BagOrder n linearly_orders Support p by A6, A7, A5, ORDERS_1:def 9; :: thesis: verum