let p be Prime; :: thesis: for R being commutative p -characteristic Ring
for a, b being Element of R holds (a + b) |^ p = (a |^ p) + (b |^ p)
let R be commutative p -characteristic Ring; :: thesis: for a, b being Element of R holds (a + b) |^ p = (a |^ p) + (b |^ p)
let a, b be Element of R; :: thesis: (a + b) |^ p = (a |^ p) + (b |^ p)
set F = (a,b) In_Power p;
len ((a,b) In_Power p) = p + 1 by BINOM:def 7;
then A0: ( ((a,b) In_Power p) . 1 = a |^ p & ((a,b) In_Power p) . (len ((a,b) In_Power p)) = b |^ p ) by BINOM:23, BINOM:24;

A1: now :: thesis: for i being Nat st 1 < i & i < len ((a,b) In_Power p) holds
((a,b) In_Power p) . i = 0. R

let i be Nat; :: thesis: ( 1 < i & i < len ((a,b) In_Power p) implies ((a,b) In_Power p) . i = 0. R )
assume B0: ( 1 < i & i < len ((a,b) In_Power p) ) ; :: thesis: ((a,b) In_Power p) . i = 0. R
then i in Seg (len ((a,b) In_Power p)) by FINSEQ_1:1;
then B1: i in dom ((a,b) In_Power p) by FINSEQ_1:def 3;
reconsider m = i - 1 as Nat by B0;
i - 1 < (len ((a,b) In_Power p)) - 1 by B0, XREAL_1:9;
then B2: m < (p + 1) - 1 by BINOM:def 7;
then p - m in NAT by INT_1:5;
then reconsider l = p - m as Nat ;
1 - 1 < m by B0, XREAL_1:9;
then B3: 0 + 1 <= m by INT_1:7;
thus ((a,b) In_Power p) . i = ((a,b) In_Power p) /. i by B1, PARTFUN1:def 6
.= ((p choose m) * (a |^ l)) * (b |^ m) by B1, BINOM:def 7
.= (0. R) * (b |^ m) by B3, B2, Lm2, NEWTON02:119
.= 0. R ; :: thesis: verum

end;

consider fp being sequence of the carrier of R such that
A2: Sum ((a,b) In_Power p) = fp . (len ((a,b) In_Power p)) and
A3: fp . 0 = 0. R and
A4: for j being Nat
for v being Element of R st j < len ((a,b) In_Power p) & v = ((a,b) In_Power p) . (j + 1) holds
fp . (j + 1) = (fp . j) + v by RLVECT_1:def 12;
defpred S₁[ Element of NAT ] means ( ( $1 = 0 & fp . $1 = 0. R ) or ( 0 < $1 & $1 < len ((a,b) In_Power p) & fp . $1 = a |^ p ) or ( $1 = len ((a,b) In_Power p) & fp . $1 = (a |^ p) + (b |^ p) ) );
IA: S₁[ 0 ] by A3;

IS: now :: thesis: for j being Element of NAT st 0 <= j & j < len ((a,b) In_Power p) & S₁[j] holds
S₁[j + 1]

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len ((a,b) In_Power p) & S₁[j] implies S₁[b₁ + 1] )
assume C1: ( 0 <= j & j < len ((a,b) In_Power p) ) ; :: thesis: ( S₁[j] implies S₁[b₁ + 1] )
assume C2: S₁[j] ; :: thesis: S₁[b₁ + 1]

per cases ( ( j = 0 & j < (len ((a,b) In_Power p)) - 1 ) or ( j = 0 & j = (len ((a,b) In_Power p)) - 1 ) or ( j = 0 & j > (len ((a,b) In_Power p)) - 1 ) or ( 0 < j & j < (len ((a,b) In_Power p)) - 1 ) or ( 0 < j & j = (len ((a,b) In_Power p)) - 1 ) or ( 0 < j & j > (len ((a,b) In_Power p)) - 1 ) ) by XXREAL_0:1;

suppose D1: ( j = 0 & j < (len ((a,b) In_Power p)) - 1 ) ; :: thesis: S₁[b₁ + 1]

then j < len ((a,b) In_Power p) ;
then D2: fp . (j + 1) = (fp . 0) + (a |^ p) by D1, A0, A4;
j + 1 < ((len ((a,b) In_Power p)) - 1) + 1 by D1, XREAL_1:6;
hence S₁[j + 1] by D2, A3; :: thesis: verum

end;

suppose ( j = 0 & j = (len ((a,b) In_Power p)) - 1 ) ; :: thesis: S₁[b₁ + 1]

then 0 + 1 = p + 1 by BINOM:def 7;
hence S₁[j + 1] ; :: thesis: verum

end;

suppose ( j = 0 & j > (len ((a,b) In_Power p)) - 1 ) ; :: thesis: S₁[b₁ + 1]

hence S₁[j + 1] by C1; :: thesis: verum

end;

suppose D1: ( 0 < j & j < (len ((a,b) In_Power p)) - 1 ) ; :: thesis: S₁[b₁ + 1]

then D3: j + 1 < ((len ((a,b) In_Power p)) - 1) + 1 by XREAL_1:6;
j + 1 > 0 + 1 by D1, XREAL_1:8;
then ((a,b) In_Power p) . (j + 1) = 0. R by D3, A1;
then fp . (j + 1) = (a |^ p) + (0. R) by A4, C2, C1, A0;
hence S₁[j + 1] by D3; :: thesis: verum

end;

suppose ( 0 < j & j = (len ((a,b) In_Power p)) - 1 ) ; :: thesis: S₁[b₁ + 1]

hence S₁[j + 1] by A0, A4, C2; :: thesis: verum

end;

suppose ( 0 < j & j > (len ((a,b) In_Power p)) - 1 ) ; :: thesis: S₁[b₁ + 1]

then j >= ((len ((a,b) In_Power p)) - 1) + 1 by INT_1:7;
hence S₁[j + 1] by C1; :: thesis: verum

end;

end;

end;

I: for j being Element of NAT st 0 <= j & j <= len ((a,b) In_Power p) holds
S₁[j] from INT_1:sch 7(IA, IS);
H: len ((a,b) In_Power p) = p + 1 by BINOM:def 7;
p is Element of NAT by ORDINAL1:def 12;
hence (a + b) |^ p = Sum ((a,b) In_Power p) by BINOM:25
.= (a |^ p) + (b |^ p) by I, A2, H ;
:: thesis: verum