let R be domRing; :: thesis: for n being Nat holds Sum (n |-> (0. R)) = 0. R
let n be Nat; :: thesis: Sum (n |-> (0. R)) = 0. R
defpred S₁[ Nat] means Sum ($1 |-> (0. R)) = 0. R;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
Sum ((n + 1) |-> (0. R)) = Sum ((n |-> (0. R)) ^ <*(0. R)*>) by FINSEQ_2:60
.= (0. R) + (0. R) by A2, FVSUM_1:71
.= 0. R ;
hence S₁[n + 1] ; :: thesis: verum

end;

A3: S₁[ 0 ]

proof

Sum (0 |-> (0. R)) = Sum (<*> the carrier of R)
.= 0. R by RLVECT_1:43 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence Sum (n |-> (0. R)) = 0. R ; :: thesis: verum