let f be complex-valued FinSequence; :: thesis: 0 (#) f = (len f) |-> 0
A1: dom (0 (#) f) = dom f by VALUED_1:def 5
.= Seg (len ((len f) |-> 0)) by FINSEQ_1:def 3
.= dom ((len f) |-> 0) ;
for c being Nat st c in dom (0 (#) f) holds
(0 (#) f) . c = ((len f) |-> 0) . c ;
hence 0 (#) f = (len f) |-> 0 by A1, FINSEQ_1:13; :: thesis: verum