let R be domRing; :: thesis: for p being Polynomial of R
for n being Nat holds LC (p `^ n) = (LC p) |^ n
let p be Polynomial of R; :: thesis: for n being Nat holds LC (p `^ n) = (LC p) |^ n
let n be Nat; :: thesis: LC (p `^ n) = (LC p) |^ n

per cases ( n is zero or not n is zero ) ;

suppose A: n is zero ; :: thesis: LC (p `^ n) = (LC p) |^ n

LC (p `^ 0) = LC (1_. R) by POLYNOM5:15
.= LC ((1. R) | R) by RING_4:14
.= 1_ R by RING_5:6
.= (LC p) |^ 0 by BINOM:8 ;
hence LC (p `^ n) = (LC p) |^ n by A; :: thesis: verum

end;

suppose A: not n is zero ; :: thesis: LC (p `^ n) = (LC p) |^ n

defpred S₁[ Nat] means LC (p `^ $1) = (LC p) |^ $1;
LC (p `^ 1) = LC p by POLYNOM5:16
.= (LC p) |^ 1 by BINOM:8 ;
then IA: S₁[1] ;

IS: now :: thesis: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]
LC (p `^ (k + 1)) = LC ((p `^ k) *' p) by POLYNOM5:19
.= (LC (p `^ k)) * (LC p) by NIVEN:46
.= ((LC p) |^ k) * ((LC p) |^ 1) by IV, BINOM:8
.= (LC p) |^ (k + 1) by BINOM:10 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(IA, IS);
hence LC (p `^ n) = (LC p) |^ n by A; :: thesis: verum

end;

end;