let f1, f2 be Polynomial of L; :: thesis: ( ex t being Polynomial of L st
( p = (f1 *' s) + t & deg t < deg s ) & ex t being Polynomial of L st
( p = (f2 *' s) + t & deg t < deg s ) implies f1 = f2 )
given t1 being Polynomial of L such that A52: p = (f1 *' s) + t1 and
A53: deg t1 < deg s ; :: thesis: ( for t being Polynomial of L holds
( not p = (f2 *' s) + t or not deg t < deg s ) or f1 = f2 )
given t2 being Polynomial of L such that A54: p = (f2 *' s) + t2 and
A55: deg t2 < deg s ; :: thesis: f1 = f2
A56: (f2 - f1) *' s = (f2 *' s) + ((- f1) *' s) by POLYNOM3:32
.= (f2 *' s) - (f1 *' s) by Th12 ;
f2 *' s = (f2 *' s) + (0_. L) by POLYNOM3:28
.= (f2 *' s) + (t2 - t2) by POLYNOM3:29
.= ((f1 *' s) + t1) + (- t2) by A52, A54, POLYNOM3:26 ;
then A57: (f2 *' s) - (f1 *' s) = ((f1 *' s) + (t1 + (- t2))) + (- (f1 *' s)) by POLYNOM3:26
.= (t1 + (- t2)) + ((f1 *' s) - (f1 *' s)) by POLYNOM3:26
.= (t1 + (- t2)) + (0_. L) by POLYNOM3:29
.= t1 - t2 by POLYNOM3:28 ;

now :: thesis: not f1 <> f2

assume A58: f1 <> f2 ; :: thesis: contradiction

A59: now :: thesis: not f2 - f1 = 0_. L

assume f2 - f1 = 0_. L ; :: thesis: contradiction
then f1 = (f2 + (- f1)) + f1 by POLYNOM3:28
.= f2 + (f1 - f1) by POLYNOM3:26
.= f2 + (0_. L) by POLYNOM3:29 ;
hence contradiction by A58, POLYNOM3:28; :: thesis: verum

end;

then reconsider d = deg (f2 - f1), degs = deg s as Nat by B1, Lm8;
deg (t1 - t2) <= max ((deg t1),(deg (- t2))) by Th22;
then A60: deg (t1 - t2) <= max ((deg t1),(deg t2)) by POLYNOM4:8;
A61: deg (t1 - t2) < degs

proof

per cases ( max ((deg t1),(deg t2)) = deg t1 or max ((deg t1),(deg t2)) = deg t2 ) by XXREAL_0:16;

suppose max ((deg t1),(deg t2)) = deg t1 ; :: thesis: deg (t1 - t2) < degs

hence deg (t1 - t2) < degs by A53, A60, XXREAL_0:2; :: thesis: verum

end;

suppose max ((deg t1),(deg t2)) = deg t2 ; :: thesis: deg (t1 - t2) < degs

hence deg (t1 - t2) < degs by A55, A60, XXREAL_0:2; :: thesis: verum

end;

end;

end;

deg (t1 - t2) = d + degs by B1, A57, A56, A59, Th23;
hence contradiction by A61, NAT_1:11; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum