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

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