let f be Complex_Sequence; :: thesis: for n being Nat holds XProduct (f | (n + 1)) = (Partial_Product f) . n
let n be Nat; :: thesis: XProduct (f | (n + 1)) = (Partial_Product f) . n
defpred S₁[ Nat] means XProduct (f | ($1 + 1)) = (Partial_Product f) . $1;
A1: S₁[ 0 ]

proof

XProduct (f | (0 + 1)) = (XProduct (f | 0)) * (f . 0) by C265
.= 1 * (f . 0) by PFO ;
hence S₁[ 0 ] by PP; :: thesis: verum

end;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: XProduct (f | (k + 1)) = (Partial_Product f) . k ; :: thesis: S₁[k + 1]
XProduct (f | ((k + 1) + 1)) = ((Partial_Product f) . k) * (f . (k + 1)) by B1, C265;
hence S₁[k + 1] by PP; :: thesis: verum

end;

for x being Nat holds S₁[x] from NAT_1:sch 2(A1, A2);
hence XProduct (f | (n + 1)) = (Partial_Product f) . n ; :: thesis: verum