let D be set ; :: thesis: for Y being FinSequenceSet of D
for F being FinSequence of Y st ( for n being Nat st n in dom F holds
F . n = <*> D ) holds
Sum (Length F) = 0
let Y be FinSequenceSet of D; :: thesis: for F being FinSequence of Y st ( for n being Nat st n in dom F holds
F . n = <*> D ) holds
Sum (Length F) = 0
let F be FinSequence of Y; :: thesis: ( ( for n being Nat st n in dom F holds
F . n = <*> D ) implies Sum (Length F) = 0 )
assume A1: for n being Nat st n in dom F holds
F . n = <*> D ; :: thesis: Sum (Length F) = 0
A2: dom (Length F) = dom F by Def1
.= Seg (len F) by FINSEQ_1:def 3 ;
A6: (len F) |-> 0 = (Seg (len F)) --> 0 by FINSEQ_2:def 2;
then A3: dom ((len F) |-> 0) = Seg (len F) by FUNCT_2:def 1;

now :: thesis: for k being Nat st k in dom (Length F) holds
(Length F) . k = ((len F) |-> 0) . k

let k be Nat; :: thesis: ( k in dom (Length F) implies (Length F) . k = ((len F) |-> 0) . k )
assume A4: k in dom (Length F) ; :: thesis: (Length F) . k = ((len F) |-> 0) . k
then k in dom F by Def1;
then F . k = <*> D by A1;
then (Length F) . k = 0 by A4, Def1;
hence (Length F) . k = ((len F) |-> 0) . k by A2, A4, A6, FUNCOP_1:7; :: thesis: verum

end;

then Length F = (len F) |-> 0 by A2, A3, FINSEQ_1:13;
hence Sum (Length F) = 0 by RVSUM_1:81; :: thesis: verum