let R be FinSequence of REAL ; :: thesis: (0 * R) " {0 } = dom R
A1: len (0 * R) = len R by FINSEQ_2:37;
A2: ( dom R = Seg (len R) & Seg (len (0 * R)) = dom (0 * R) ) by FINSEQ_1:def 3;
hence (0 * R) " {0 } c= dom R by A1, RELAT_1:167; :: according to XBOOLE_0:def 10 :: thesis: dom R c= (0 * R) " {0 }
let x be set ; :: 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:66
.= 0 ;
then (0 * R) . i in {0 } by TARSKI:def 1;
hence x in (0 * R) " {0 } by A1, A2, A3, FUNCT_1:def 13; :: thesis: verum