A1: rng (f,x := r) c= REAL

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f,x := r) or y in REAL )
A2: rng (f,x := r) c= (rng f) \/ {r} by FUNCT_7:102;
assume y in rng (f,x := r) ; :: thesis: y in REAL
then ( y in rng f or y in {r} ) by A2, XBOOLE_0:def 3;
hence y in REAL ; :: thesis: verum

end;

dom (f,x := r) = dom f by FUNCT_7:32
.= Seg (len f) by FINSEQ_1:def 3 ;
then f,x := r is FinSequence by FINSEQ_1:def 2;
hence f,x := r is FinSequence of REAL by A1, FINSEQ_1:def 4; :: thesis: verum