let n be Nat; :: thesis: for k being Element of NAT holds Sum (k |-> (0* n)) = 0* n
let k be Element of 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:19;
hence (k |-> (0* n)) . i = 0* n by FINSEQ_2:71; :: 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

then consider g3 being FinSequence of REAL n such that
A3: ( len (k |-> (0* n)) = len g3 & (k |-> (0* n)) . 1 = g3 . 1 & ( for i being Nat st 1 <= i & i < len (k |-> (0* n)) holds
g3 . (i + 1) = (g3 /. i) + ((k |-> (0* n)) /. (i + 1)) ) & Sum (k |-> (0* n)) = g3 . (len (k |-> (0* n))) ) by Def11;
defpred S₁[ Nat] means ( $1 < len (k |-> (0* n)) implies g3 . ($1 + 1) = 0* n );
A4: 0 + 1 <= len (k |-> (0* n)) by A2, NAT_1:13;
then 1 in Seg (len (k |-> (0* n))) by FINSEQ_1:3;
then 1 in dom (k |-> (0* n)) by FINSEQ_1:def 3;
then A5: S₁[ 0 ] by A1, A3;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

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

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

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

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

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

then A12: g3 . ((k + 1) + 1) = (g3 /. (k + 1)) + ((k |-> (0* n)) /. ((k + 1) + 1)) by A3, A9;
A13: g3 /. (k + 1) = g3 . (k + 1) by A11, A9, A3, FINSEQ_4:24;
A14: 1 <= (k + 1) + 1 by XREAL_1:31;
then (k + 1) + 1 in Seg (len (k |-> (0* n))) by A10, FINSEQ_1:3;
then (k + 1) + 1 in dom (k |-> (0* n)) by FINSEQ_1:def 3;
then (k |-> (0* n)) . ((k + 1) + 1) = 0* n by A1;
then g3 . ((k + 1) + 1) = (0* n) + (0* n) by A7, A8, A9, A10, A12, A13, A14, FINSEQ_4:24, 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;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
then A15: S₁[(len g3) -' 1] ;
(len g3) -' 1 = (len g3) - 1 by A3, A4, XREAL_1:235;
hence Sum (k |-> (0* n)) = 0* n by A3, A15, XREAL_1:46; :: 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;