let n, k be Nat; :: thesis: Sum (k |-> (0* n)) = 0* n
set g = k |-> (0* n);
A1: for i being Nat st i in dom (k |-> (0* n)) holds
(k |-> (0* n)) . i = 0* n

proof

let i be Nat; :: thesis: ( i in dom (k |-> (0* n)) implies (k |-> (0* n)) . i = 0* n )
assume i in dom (k |-> (0* n)) ; :: thesis: (k |-> (0* n)) . i = 0* n
then i in Seg k by FUNCOP_1:13;
hence (k |-> (0* n)) . i = 0* n by FINSEQ_2:57; :: thesis: verum

end;

per cases ( len (k |-> (0* n)) > 0 or len (k |-> (0* n)) <= 0 ) ;

suppose A2: len (k |-> (0* n)) > 0 ; :: thesis: Sum (k |-> (0* n)) = 0* n

set g3 = accum (k |-> (0* n));
A3: len (k |-> (0* n)) = len (accum (k |-> (0* n))) by Def10;
A4: (k |-> (0* n)) . 1 = (accum (k |-> (0* n))) . 1 by Def10;
defpred S₁[ Nat] means ( $1 < len (k |-> (0* n)) implies (accum (k |-> (0* n))) . ($1 + 1) = 0* n );
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
A7: k < k + 1 by XREAL_1:29;

per cases ( k + 1 < len (k |-> (0* n)) or k + 1 >= len (k |-> (0* n)) ) ;

suppose A8: k + 1 < len (k |-> (0* n)) ; :: thesis: S₁[k + 1]

then A9: (k + 1) + 1 <= len (k |-> (0* n)) by NAT_1:13;

per cases ( 1 <= k + 1 or 1 > k + 1 ) ;

suppose A10: 1 <= k + 1 ; :: thesis: S₁[k + 1]

A11: 1 <= (k + 1) + 1 by XREAL_1:29;
then (k + 1) + 1 in Seg (len (k |-> (0* n))) by A9, FINSEQ_1:1;
then (k + 1) + 1 in dom (k |-> (0* n)) by FINSEQ_1:def 3;
then A12: (k |-> (0* n)) . ((k + 1) + 1) = 0* n by A1;
A13: (accum (k |-> (0* n))) /. (k + 1) = (accum (k |-> (0* n))) . (k + 1) by A3, A8, A10, FINSEQ_4:15;
(accum (k |-> (0* n))) . ((k + 1) + 1) = ((accum (k |-> (0* n))) /. (k + 1)) + ((k |-> (0* n)) /. ((k + 1) + 1)) by Def10, A8, A10;
then (accum (k |-> (0* n))) . ((k + 1) + 1) = (0* n) + (0* n) by A6, A7, A8, A9, A13, A11, A12, FINSEQ_4:15, XXREAL_0:2
.= 0* n by EUCLID_4:1 ;
hence S₁[k + 1] ; :: thesis: verum

end;

suppose 1 > k + 1 ; :: thesis: S₁[k + 1]

hence S₁[k + 1] by NAT_1:14; :: thesis: verum

end;

end;

end;

suppose k + 1 >= len (k |-> (0* n)) ; :: thesis: S₁[k + 1]

hence S₁[k + 1] ; :: thesis: verum

end;

end;

end;

A14: 0 + 1 <= len (k |-> (0* n)) by A2, NAT_1:13;
then 1 in Seg (len (k |-> (0* n))) by FINSEQ_1:1;
then 1 in dom (k |-> (0* n)) by FINSEQ_1:def 3;
then A15: S₁[ 0 ] by A1, A4;
for k being Nat holds S₁[k] from NAT_1:sch 2(A15, A5);
then A16: S₁[(len (accum (k |-> (0* n)))) -' 1] ;
(len (accum (k |-> (0* n)))) -' 1 = (len (accum (k |-> (0* n)))) - 1 by A3, A14, XREAL_1:233;
hence Sum (k |-> (0* n)) = 0* n by A3, Def11, A16, XREAL_1:44; :: thesis: verum

end;

suppose len (k |-> (0* n)) <= 0 ; :: thesis: Sum (k |-> (0* n)) = 0* n

hence Sum (k |-> (0* n)) = 0* n by Def11; :: thesis: verum

end;

end;