A1: rng ((f,x) := r) c= REAL
proof
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;
dom ((f,x) := r) = dom f by FUNCT_7:30
.= 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