:: POLYNOM6 semantic presentation
theorem Th1: :: POLYNOM6:1
for
b1,
b2 being
Ordinal for
b3 being
set st ( for
b4 being
set holds
(
b4 in b3 iff ex
b5 being
Ordinal st
(
b4 = b1 +^ b5 &
b5 in b2 ) ) ) holds
b1 +^ b2 = b1 \/ b3
theorem Th2: :: POLYNOM6:2
for
b1 being
Ordinal for
b2,
b3 being
bag of
b1 st
b2 < b3 holds
ex
b4 being
Ordinal st
(
b4 in b1 &
b2 . b4 < b3 . b4 & ( for
b5 being
Ordinal st
b5 in b4 holds
b2 . b5 = b3 . b5 ) )
:: deftheorem Def1 defines +^ POLYNOM6:def 1 :
theorem Th3: :: POLYNOM6:3
theorem Th4: :: POLYNOM6:4
theorem Th5: :: POLYNOM6:5
theorem Th6: :: POLYNOM6:6
theorem Th7: :: POLYNOM6:7
theorem Th8: :: POLYNOM6:8
definition
let c1,
c2 be non
empty Ordinal;
let c3 be non
empty add-associative right_zeroed right_complementable unital distributive non
trivial doubleLoopStr ;
let c4 be
Polynomial of
c1,
(Polynom-Ring c2,c3);
func Compress c4 -> Polynomial of
(a1 +^ a2),
a3 means :
Def2:
:: POLYNOM6:def 2
for
b1 being
Element of
Bags (a1 +^ a2) ex
b2 being
Element of
Bags a1ex
b3 being
Element of
Bags a2ex
b4 being
Polynomial of
a2,
a3 st
(
b4 = a4 . b2 &
b1 = b2 +^ b3 &
a5 . b1 = b4 . b3 );
existence
ex b1 being Polynomial of (c1 +^ c2),c3 st
for b2 being Element of Bags (c1 +^ c2) ex b3 being Element of Bags c1ex b4 being Element of Bags c2ex b5 being Polynomial of c2,c3 st
( b5 = c4 . b3 & b2 = b3 +^ b4 & b1 . b2 = b5 . b4 )
uniqueness
for b1, b2 being Polynomial of (c1 +^ c2),c3 st ( for b3 being Element of Bags (c1 +^ c2) ex b4 being Element of Bags c1ex b5 being Element of Bags c2ex b6 being Polynomial of c2,c3 st
( b6 = c4 . b4 & b3 = b4 +^ b5 & b1 . b3 = b6 . b5 ) ) & ( for b3 being Element of Bags (c1 +^ c2) ex b4 being Element of Bags c1ex b5 being Element of Bags c2ex b6 being Polynomial of c2,c3 st
( b6 = c4 . b4 & b3 = b4 +^ b5 & b2 . b3 = b6 . b5 ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines Compress POLYNOM6:def 2 :
theorem Th9: :: POLYNOM6:9
theorem Th10: :: POLYNOM6:10
theorem Th11: :: POLYNOM6:11
theorem Th12: :: POLYNOM6:12
theorem Th13: :: POLYNOM6:13
theorem Th14: :: POLYNOM6:14
theorem Th15: :: POLYNOM6:15