let f be finite-support Function; :: thesis: rng f c= (rng (f | (support f))) \/ {0}
set g = f | (support f);
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in (rng (f | (support f))) \/ {0} )
assume y in rng f ; :: thesis: y in (rng (f | (support f))) \/ {0}
then consider x being object such that
A1: x in dom f and
A2: f . x = y by FUNCT_1:def 3;

per cases ( f . x = 0 or f . x <> 0 ) ;

suppose f . x = 0 ; :: thesis: y in (rng (f | (support f))) \/ {0}

then f . x in {0} by TARSKI:def 1;
hence y in (rng (f | (support f))) \/ {0} by A2, XBOOLE_0:def 3; :: thesis: verum

end;

suppose f . x <> 0 ; :: thesis: y in (rng (f | (support f))) \/ {0}

then A3: x in support f by PRE_POLY:def 7;
then A4: f . x = (f | (support f)) . x by FUNCT_1:49;
x in dom (f | (support f)) by A1, A3, RELAT_1:57;
then (f | (support f)) . x in rng (f | (support f)) by FUNCT_1:def 3;
hence y in (rng (f | (support f))) \/ {0} by A2, A4, XBOOLE_0:def 3; :: thesis: verum

end;

end;