defpred S₁[ Nat] means (Partial_Product (seq_const c)) . $1 = c |^ ($1 + 1);
A1: S₁[ 0 ]

proof

(Partial_Product (seq_const c)) . 0 = (seq_const c) . 0 by PP
.= c |^ (0 + 1) ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: for l being Nat st S₁[l] holds
S₁[l + 1]

proof

let l be Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume A3: S₁[l] ; :: thesis: S₁[l + 1]
(Partial_Product (seq_const c)) . (l + 1) = ((Partial_Product (seq_const c)) . l) * ((seq_const c) . (l + 1)) by PP
.= c |^ ((l + 1) + 1) by A3, NEWTON:6 ;
hence S₁[l + 1] ; :: thesis: verum

end;

A4: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
for j being non zero Nat holds (Partial_Product (seq_const c)) . (j - 1) = c |^ j

proof

let j be non zero Nat; :: thesis: (Partial_Product (seq_const c)) . (j - 1) = c |^ j
reconsider x = j - 1 as Nat ;
(Partial_Product (seq_const c)) . x = c |^ (x + 1) by A4
.= c |^ j ;
hence (Partial_Product (seq_const c)) . (j - 1) = c |^ j ; :: thesis: verum

end;

hence for b₁ being set holds
( b₁ = c |^ n iff b₁ = (Partial_Product (seq_const c)) . (n - 1) ) ; :: thesis: verum