let B, C, D, b, c, d be set ; :: thesis: for h being Function st h = ((B .--> b) +* (C .--> c)) +* (D .--> d) holds
rng h = {(h . B),(h . C),(h . D)}
let h be Function; :: thesis: ( h = ((B .--> b) +* (C .--> c)) +* (D .--> d) implies rng h = {(h . B),(h . C),(h . D)} )
assume h = ((B .--> b) +* (C .--> c)) +* (D .--> d) ; :: thesis: rng h = {(h . B),(h . C),(h . D)}
then A1: dom h = {B,C,D} by Lm1;
then A2: B in dom h by ENUMSET1:def 1;
A3: rng h c= {(h . B),(h . C),(h . D)}

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in rng h or t in {(h . B),(h . C),(h . D)} )
assume t in rng h ; :: thesis: t in {(h . B),(h . C),(h . D)}
then consider x1 being set such that
A4: x1 in dom h and
A5: t = h . x1 by FUNCT_1:def 5;

now

per cases ( x1 = D or x1 = B or x1 = C ) by A1, A4, ENUMSET1:def 1;

case x1 = D ; :: thesis: t in {(h . B),(h . C),(h . D)}

hence t in {(h . B),(h . C),(h . D)} by A5, ENUMSET1:def 1; :: thesis: verum

end;

case x1 = B ; :: thesis: t in {(h . B),(h . C),(h . D)}

hence t in {(h . B),(h . C),(h . D)} by A5, ENUMSET1:def 1; :: thesis: verum

end;

case x1 = C ; :: thesis: t in {(h . B),(h . C),(h . D)}

hence t in {(h . B),(h . C),(h . D)} by A5, ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

hence t in {(h . B),(h . C),(h . D)} ; :: thesis: verum

end;

A6: C in dom h by A1, ENUMSET1:def 1;
A7: D in dom h by A1, ENUMSET1:def 1;
{(h . B),(h . C),(h . D)} c= rng h

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in {(h . B),(h . C),(h . D)} or t in rng h )
assume A8: t in {(h . B),(h . C),(h . D)} ; :: thesis: t in rng h

now

per cases ( t = h . D or t = h . B or t = h . C ) by A8, ENUMSET1:def 1;

case t = h . D ; :: thesis: t in rng h

hence t in rng h by A7, FUNCT_1:def 5; :: thesis: verum

end;

case t = h . B ; :: thesis: t in rng h

hence t in rng h by A2, FUNCT_1:def 5; :: thesis: verum

end;

case t = h . C ; :: thesis: t in rng h

hence t in rng h by A6, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence t in rng h ; :: thesis: verum

end;

hence rng h = {(h . B),(h . C),(h . D)} by A3, XBOOLE_0:def 10; :: thesis: verum