let k, n be Nat; :: thesis: for R being commutative Ring
for z0, z1 being Element of R holds
( (<%z0,z1%> `^ 0) . 0 = 1. R & ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )
let R be commutative Ring; :: thesis: for z0, z1 being Element of R holds
( (<%z0,z1%> `^ 0) . 0 = 1. R & ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )
let z0, z1 be Element of R; :: thesis: ( (<%z0,z1%> `^ 0) . 0 = 1. R & ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )
<%z0,z1%> `^ 0 = 1_. R by POLYNOM5:15;
hence (<%z0,z1%> `^ 0) . 0 = 1. R by POLYNOM3:30; :: thesis: ( ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )
set P = <%(0. R),z1%>;
defpred S1[ Nat] means ( ( $1 > 0 implies (<%(0. R),z1%> `^ $1) . $1 = z1 |^ $1 ) & ( for k being Nat st k <> $1 holds
(<%(0. R),z1%> `^ $1) . k = 0. R ) );
A1: S1[ 0 ]
proof
thus ( 0 > 0 implies (<%(0. R),z1%> `^ 0) . 0 = z1 |^ 0 ) ; :: thesis: for k being Nat st k <> 0 holds
(<%(0. R),z1%> `^ 0) . k = 0. R
let k be Nat; :: thesis: ( k <> 0 implies (<%(0. R),z1%> `^ 0) . k = 0. R )
assume A2: k <> 0 ; :: thesis: (<%(0. R),z1%> `^ 0) . k = 0. R
<%(0. R),z1%> `^ 0 = 1_. R by POLYNOM5:15;
hence (<%(0. R),z1%> `^ 0) . k = 0. R by A2, POLYNOM3:30; :: thesis: verum
end;
A3: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
set i1 = i + 1;
assume A4: S1[i] ; :: thesis: S1[i + 1]
A5: <%(0. R),z1%> `^ (i + 1) = (<%(0. R),z1%> `^ i) *' <%(0. R),z1%> by POLYNOM5:19;
thus ( i + 1 > 0 implies (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 |^ (i + 1) ) :: thesis: for k being Nat st k <> i + 1 holds
(<%(0. R),z1%> `^ (i + 1)) . k = 0. R
proof
assume i + 1 > 0 ; :: thesis: (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 |^ (i + 1)
per cases ( i = 0 or i > 0 ) ;
suppose A6: i = 0 ; :: thesis: (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 |^ (i + 1)
then <%(0. R),z1%> `^ (i + 1) = <%(0. R),z1%> by POLYNOM5:16;
hence (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 by A6, POLYNOM5:38
.= z1 |^ (i + 1) by A6, BINOM:8 ;
:: thesis: verum
end;
suppose A7: i > 0 ; :: thesis: (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 |^ (i + 1)
consider r being FinSequence of the carrier of R such that
A8: ( len r = (i + 1) + 1 & (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = Sum r ) and
A9: for k being Element of NAT st k in dom r holds
r . k = ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . (((i + 1) + 1) -' k)) by A5, POLYNOM3:def 9;
A10: ( 1 <= i + 1 & i + 1 <= len r ) by A8, NAT_1:11;
then A11: i + 1 in dom r by FINSEQ_3:25;
for k being Element of NAT st k in dom r & k <> i + 1 holds
r /. k = 0. R
proof
let k be Element of NAT ; :: thesis: ( k in dom r & k <> i + 1 implies r /. k = 0. R )
assume A12: ( k in dom r & k <> i + 1 ) ; :: thesis: r /. k = 0. R
A13: k <= (i + 1) + 1 by A8, A12, FINSEQ_3:25;
A14: r /. k = r . k by PARTFUN1:def 6, A12;
per cases ( k > i + 1 or k < i + 1 ) by A12, XXREAL_0:1;
suppose k > i + 1 ; :: thesis: r /. k = 0. R
then k >= (i + 1) + 1 by NAT_1:13;
then k = (i + 1) + 1 by A13, XXREAL_0:1;
then ((i + 1) + 1) -' k = 0 by XREAL_1:232;
then <%(0. R),z1%> . (((i + 1) + 1) -' k) = 0. R by POLYNOM5:38;
then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . (((i + 1) + 1) -' k)) = 0. R ;
hence r /. k = 0. R by A14, A12, A9; :: thesis: verum
end;
suppose A15: k < i + 1 ; :: thesis: r /. k = 0. R
then k < (i + 1) + 1 by NAT_1:13;
then A16: ((i + 1) + 1) -' k = ((i + 1) + 1) - k by XREAL_1:233;
k <= i by A15, NAT_1:13;
then i - k >= 0 by XREAL_1:48;
then (i - k) + 2 >= 0 + 2 by XREAL_1:6;
then <%(0. R),z1%> . (((i + 1) + 1) -' k) = 0. R by A16, POLYNOM5:38;
then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . (((i + 1) + 1) -' k)) = 0. R ;
hence r /. k = 0. R by A14, A12, A9; :: thesis: verum
end;
end;
end;
then A17: Sum r = r /. (i + 1) by A10, FINSEQ_3:25, POLYNOM2:3;
( (i + 1) -' 1 = (i + 1) - 1 & ((i + 1) + 1) -' (i + 1) = ((i + 1) + 1) - (i + 1) ) by NAT_1:11, XREAL_1:233;
then ( (<%(0. R),z1%> `^ i) . ((i + 1) -' 1) = z1 |^ i & <%(0. R),z1%> . (((i + 1) + 1) -' (i + 1)) = z1 ) by A7, A4, POLYNOM5:38;
then ( r . (i + 1) = (z1 |^ i) * z1 & z1 = z1 |^ 1 ) by A9, A10, FINSEQ_3:25, BINOM:8;
then r . (i + 1) = z1 |^ (i + 1) by BINOM:10;
hence (<%(0. R),z1%> `^ (i + 1)) . (i + 1) = z1 |^ (i + 1) by A17, A8, A11, PARTFUN1:def 6; :: thesis: verum
end;
end;
end;
let j be Nat; :: thesis: ( j <> i + 1 implies (<%(0. R),z1%> `^ (i + 1)) . j = 0. R )
assume A18: j <> i + 1 ; :: thesis: (<%(0. R),z1%> `^ (i + 1)) . j = 0. R
set j1 = j + 1;
j in NAT by ORDINAL1:def 12;
then consider r being FinSequence of the carrier of R such that
A19: ( len r = j + 1 & (<%(0. R),z1%> `^ (i + 1)) . j = Sum r ) and
A20: for k being Element of NAT st k in dom r holds
r . k = ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . ((j + 1) -' k)) by A5, POLYNOM3:def 9;
for k being Element of NAT st k in dom r holds
r . k = 0. R
proof
let k be Element of NAT ; :: thesis: ( k in dom r implies r . k = 0. R )
assume A21: k in dom r ; :: thesis: r . k = 0. R
A22: ( 1 <= k & k <= j + 1 ) by A19, A21, FINSEQ_3:25;
per cases ( k = j or k > j or k < j ) by XXREAL_0:1;
suppose k = j ; :: thesis: r . k = 0. R
then k -' 1 = j - 1 by A22, XREAL_1:233;
then k -' 1 <> i by A18;
then (<%(0. R),z1%> `^ i) . (k -' 1) = 0. R by A4;
then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . ((j + 1) -' k)) = 0. R ;
hence r . k = 0. R by A21, A20; :: thesis: verum
end;
suppose k > j ; :: thesis: r . k = 0. R
then k >= j + 1 by NAT_1:13;
then k = j + 1 by A22, XXREAL_0:1;
then (j + 1) -' k = 0 by XREAL_1:232;
then <%(0. R),z1%> . ((j + 1) -' k) = 0. R by POLYNOM5:38;
then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . ((j + 1) -' k)) = 0. R ;
hence r . k = 0. R by A21, A20; :: thesis: verum
end;
suppose A23: k < j ; :: thesis: r . k = 0. R
then k < j + 1 by NAT_1:13;
then A24: (j + 1) -' k = (j + 1) - k by XREAL_1:233;
j - k > 0 by A23, XREAL_1:50;
then (j - k) + 1 > 0 + 1 by XREAL_1:6;
then (j + 1) -' k >= 1 + 1 by NAT_1:13, A24;
then <%(0. R),z1%> . ((j + 1) -' k) = 0. R by POLYNOM5:38;
then ((<%(0. R),z1%> `^ i) . (k -' 1)) * (<%(0. R),z1%> . ((j + 1) -' k)) = 0. R ;
hence r . k = 0. R by A21, A20; :: thesis: verum
end;
end;
end;
hence (<%(0. R),z1%> `^ (i + 1)) . j = 0. R by A19, POLYNOM3:1; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A1, A3);
 hence ( ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) ) ; :: thesis: verum