let n be Nat; :: thesis: for K being non empty right_complementable add-associative right_zeroed addLoopStr holds Sum (n |-> (0. K)) = 0. K
let K be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: Sum (n |-> (0. K)) = 0. K
set p = n |-> (0. K);
for i being Element of NAT st i in dom (n |-> (0. K)) holds
(n |-> (0. K)) . i = 0. K

proof

let i be Element of NAT ; :: thesis: ( i in dom (n |-> (0. K)) implies (n |-> (0. K)) . i = 0. K )
assume i in dom (n |-> (0. K)) ; :: thesis: (n |-> (0. K)) . i = 0. K
then i in Seg n by FUNCOP_1:13;
hence (n |-> (0. K)) . i = 0. K by FUNCOP_1:7; :: thesis: verum

end;

hence Sum (n |-> (0. K)) = 0. K by Lm1; :: thesis: verum