set f = <*a,b,c*>;
( len <*a,b,c*> = 3 & <*a,b,c*> . 1 = a & <*a,b,c*> . 2 = b & <*a,b,c*> . 3 = c ) by FINSEQ_1:45;
then A2: dom <*a,b,c*> = Seg 3 by FINSEQ_1:def 3
.= (Seg 2) \/ {(2 + 1)} by FINSEQ_1:9
.= {1,2} \/ {3} by FINSEQ_1:2 ;

now :: thesis: for o being object st o in rng <*a,b,c*> holds
o in the carrier of R

let o be object ; :: thesis: ( o in rng <*a,b,c*> implies b₁ in the carrier of R )
assume o in rng <*a,b,c*> ; :: thesis: b₁ in the carrier of R
then consider y being object such that
B: ( y in dom <*a,b,c*> & <*a,b,c*> . y = o ) by FUNCT_1:def 3;

per cases ( y in {1,2} or y in {3} ) by B, A2, XBOOLE_0:def 3;

suppose y in {1,2} ; :: thesis: b₁ in the carrier of R

per cases then ( y = 1 or y = 2 ) by TARSKI:def 2;

suppose y = 1 ; :: thesis: b₁ in the carrier of R

hence o in the carrier of R by B; :: thesis: verum

end;

suppose y = 2 ; :: thesis: b₁ in the carrier of R

hence o in the carrier of R by B; :: thesis: verum

end;

end;

end;

suppose y in {3} ; :: thesis: b₁ in the carrier of R

then y = 3 by TARSKI:def 1;
hence o in the carrier of R by B; :: thesis: verum

end;

end;

end;

then rng <*a,b,c*> c= the carrier of R ;
hence <*a,b,c*> is the carrier of R -valued by RELAT_1:def 19; :: thesis: verum