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 A53: p = (f1 *' s) + t1 and
A54: 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 A55: p = (f2 *' s) + t2 and
A56: deg t2 < deg s ; :: thesis: f1 = f2
A57: (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 A53, A55, POLYNOM3:26 ;
then A58: (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 A59: f1 <> f2 ; :: thesis: contradiction
A60: 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 A59, POLYNOM3:28; :: thesis: verum
end;
then reconsider d = deg (f2 - f1), degs = deg s as Nat by A1, Lm8;
deg (t1 - t2) <= max ((deg t1),(deg (- t2))) by Th22;
then A61: deg (t1 - t2) <= max ((deg t1),(deg t2)) by POLYNOM4:8;
A62: 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 A54, A61, 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 A56, A61, XXREAL_0:2; :: thesis: verum
end;
end;
end;
deg (t1 - t2) = d + degs by A1, A58, A57, A60, Th23;
hence contradiction by A62, NAT_1:11; :: thesis: verum
end;
hence f1 = f2 ; :: thesis: verum