let n be Nat; :: thesis: Sum (n |-> (0. Z_2)) = 0. Z_2
set x = n |-> (0. Z_2);
A1: len (n |-> (0. Z_2)) = len (n |-> (0. Z_2)) ;

now :: thesis: for k being Nat st k in dom (n |-> (0. Z_2)) holds
(n |-> (0. Z_2)) . k = ((n |-> (0. Z_2)) /. k) + ((n |-> (0. Z_2)) /. k)

let k be Nat; :: thesis: ( k in dom (n |-> (0. Z_2)) implies (n |-> (0. Z_2)) . k = ((n |-> (0. Z_2)) /. k) + ((n |-> (0. Z_2)) /. k) )
assume k in dom (n |-> (0. Z_2)) ; :: thesis: (n |-> (0. Z_2)) . k = ((n |-> (0. Z_2)) /. k) + ((n |-> (0. Z_2)) /. k)
then (n |-> (0. Z_2)) /. k = (n |-> (0. Z_2)) . k by PARTFUN1:def 6
.= 0. Z_2 by BSPACE:5 ;
hence (n |-> (0. Z_2)) . k = ((n |-> (0. Z_2)) /. k) + ((n |-> (0. Z_2)) /. k) by BSPACE:5; :: thesis: verum

end;

then A2: (Sum (n |-> (0. Z_2))) - (Sum (n |-> (0. Z_2))) = ((Sum (n |-> (0. Z_2))) + (Sum (n |-> (0. Z_2)))) - (Sum (n |-> (0. Z_2))) by A1, RLVECT_2:2;
((Sum (n |-> (0. Z_2))) + (Sum (n |-> (0. Z_2)))) - (Sum (n |-> (0. Z_2))) = (Sum (n |-> (0. Z_2))) + ((Sum (n |-> (0. Z_2))) - (Sum (n |-> (0. Z_2)))) by RLVECT_1:28
.= (Sum (n |-> (0. Z_2))) + (0. Z_2) by RLVECT_1:15
.= Sum (n |-> (0. Z_2)) by BSPACE:5 ;
hence Sum (n |-> (0. Z_2)) = 0. Z_2 by A2, RLVECT_1:15; :: thesis: verum