let R be FinSequence of REAL ; :: thesis: (0 * R) " {0} = dom R
A1: Seg (len (0 * R)) = dom (0 * R) by FINSEQ_1:def 3;
A2: ( len (0 * R) = len R & dom R = Seg (len R) ) by FINSEQ_1:def 3, FINSEQ_2:33;
hence (0 * R) " {0} c= dom R by A1, RELAT_1:132; :: according to XBOOLE_0:def 10 :: thesis: dom R c= (0 * R) " {0}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom R or x in (0 * R) " {0} )
assume A3: x in dom R ; :: thesis: x in (0 * R) " {0}
then reconsider i = x as Element of NAT ;
(0 * R) . i = 0 * (R . i) by RVSUM_1:44
.= 0 ;
then (0 * R) . i in {0} by TARSKI:def 1;
hence x in (0 * R) " {0} by A2, A1, A3, FUNCT_1:def 7; :: thesis: verum