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

.= 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

proof

dom ((f,x) := r) =
dom f
by FUNCT_7:30
let y be object ; :: 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:100;

A3: r in REAL by XREAL_0:def 1;

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 by A3, TARSKI:def 1; :: thesis: verum

end;A2: rng ((f,x) := r) c= (rng f) \/ {r} by FUNCT_7:100;

A3: r in REAL by XREAL_0:def 1;

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 by A3, TARSKI:def 1; :: thesis: verum

.= 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