let F be Field; :: thesis: for m1, m2 being Ordinal st m1 in card (nonConstantPolys F) & m2 in card (nonConstantPolys F) holds
for p1, p2 being non constant Polynomial of F st Poly (m1,p1) = Poly (m2,p2) holds
( m1 = m2 & p1 = p2 )
let m1, m2 be Ordinal; :: thesis: ( m1 in card (nonConstantPolys F) & m2 in card (nonConstantPolys F) implies for p1, p2 being non constant Polynomial of F st Poly (m1,p1) = Poly (m2,p2) holds
( m1 = m2 & p1 = p2 ) )
assume A: ( m1 in card (nonConstantPolys F) & m2 in card (nonConstantPolys F) ) ; :: thesis: for p1, p2 being non constant Polynomial of F st Poly (m1,p1) = Poly (m2,p2) holds
( m1 = m2 & p1 = p2 )
let p1, p2 be non constant Polynomial of F; :: thesis: ( Poly (m1,p1) = Poly (m2,p2) implies ( m1 = m2 & p1 = p2 ) )
set n = card (nonConstantPolys F);
assume B: Poly (m1,p1) = Poly (m2,p2) ; :: thesis: ( m1 = m2 & p1 = p2 )
H: ( Support (Poly (m1,p1)) c= {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m1} } & Support (Poly (m2,p2)) c= {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m2} } ) by Th14c;
ex b being bag of card (nonConstantPolys F) st
( b in Support (Poly (m1,p1)) & b in Support (Poly (m2,p2)) & b <> EmptyBag (card (nonConstantPolys F)) )

proof

p1 <> 0_. F ;
then B0: Poly (m1,p1) <> 0_ ((card (nonConstantPolys F)),F) by A, pZero;
deg p1 > 0 by RATFUNC1:def 2;
then p1 is non constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4, POLYNOM3:def 10;
then B2: Support (Poly (m1,p1)) <> {(EmptyBag (card (nonConstantPolys F)))} by A, bij3a;

now :: thesis: ex b being object st
( b in Support (Poly (m1,p1)) & b <> EmptyBag (card (nonConstantPolys F)) )

assume C0: for b being object holds
( not b in Support (Poly (m1,p1)) or not b <> EmptyBag (card (nonConstantPolys F)) ) ; :: thesis: contradiction

now :: thesis: for o being object st o in Support (Poly (m1,p1)) holds
o in {(EmptyBag (card (nonConstantPolys F)))}

let o be object ; :: thesis: ( o in Support (Poly (m1,p1)) implies o in {(EmptyBag (card (nonConstantPolys F)))} )
assume o in Support (Poly (m1,p1)) ; :: thesis: o in {(EmptyBag (card (nonConstantPolys F)))}
then o = EmptyBag (card (nonConstantPolys F)) by C0;
hence o in {(EmptyBag (card (nonConstantPolys F)))} by TARSKI:def 1; :: thesis: verum

end;

then Support (Poly (m1,p1)) c= {(EmptyBag (card (nonConstantPolys F)))} ;
hence contradiction by B0, YY, B2, lemSet; :: thesis: verum

end;

then consider b being object such that
B3: ( b in Support (Poly (m1,p1)) & b <> EmptyBag (card (nonConstantPolys F)) ) ;
reconsider b = b as bag of card (nonConstantPolys F) by B3;
thus ex b being bag of card (nonConstantPolys F) st
( b in Support (Poly (m1,p1)) & b in Support (Poly (m2,p2)) & b <> EmptyBag (card (nonConstantPolys F)) ) by B3, B; :: thesis: verum

end;

then consider b being bag of card (nonConstantPolys F) such that
D0: ( b in Support (Poly (m1,p1)) & b in Support (Poly (m2,p2)) & b <> EmptyBag (card (nonConstantPolys F)) ) ;
( b in {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m1} } & not b in {(EmptyBag (card (nonConstantPolys F)))} ) by D0, H, TARSKI:def 1;
then b in { b where b is bag of card (nonConstantPolys F) : support b = {m1} } by XBOOLE_0:def 3;
then consider b1 being bag of card (nonConstantPolys F) such that
D1: ( b = b1 & support b1 = {m1} ) ;
( b in {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m2} } & not b in {(EmptyBag (card (nonConstantPolys F)))} ) by D0, H, TARSKI:def 1;
then b in { b where b is bag of card (nonConstantPolys F) : support b = {m2} } by XBOOLE_0:def 3;
then consider b2 being bag of card (nonConstantPolys F) such that
D2: ( b = b2 & support b2 = {m2} ) ;
m1 in {m2} by D1, D2, TARSKI:def 1;
hence X: m1 = m2 by TARSKI:def 1; :: thesis: p1 = p2

now :: thesis: for i being Element of NAT holds p1 . i = p2 . i

let i be Element of NAT ; :: thesis: p1 . b₁ = p2 . b₁

per cases ( i = 0 or i <> 0 ) ;

suppose E: i = 0 ; :: thesis: p1 . b₁ = p2 . b₁

hence p1 . i = (Poly (m2,p2)) . (EmptyBag (card (nonConstantPolys F))) by B, defPg
.= p2 . i by E, defPg ;
:: thesis: verum

end;

suppose C: i <> 0 ; :: thesis: p1 . b₁ = p2 . b₁

for o being object st o in {m1} holds
o in card (nonConstantPolys F) by A, TARSKI:def 1;
then reconsider S = {m1} as finite Subset of (card (nonConstantPolys F)) by TARSKI:def 3;
set b = (S,i) -bag ;
E: support ((S,i) -bag) = S by C, UPROOTS:8;
F: m1 in {m1} by TARSKI:def 1;
hence p1 . i = p1 . (((S,i) -bag) . m1) by UPROOTS:7
.= (Poly (m2,p2)) . ((S,i) -bag) by E, B, defPg
.= p2 . (((S,i) -bag) . m2) by E, X, defPg
.= p2 . i by F, UPROOTS:7, X ;
:: thesis: verum

end;

end;

end;

hence p1 = p2 ; :: thesis: verum