let B, C, D, b, c, d be object ; :: thesis: for h being Function st h = (B,C,D) --> (b,c,d) holds
rng h = {(h . B),(h . C),(h . D)}
let h be Function; :: thesis: ( h = (B,C,D) --> (b,c,d) implies rng h = {(h . B),(h . C),(h . D)} )
assume h = (B,C,D) --> (b,c,d) ; :: thesis: rng h = {(h . B),(h . C),(h . D)}
then A1: dom h = {B,C,D} by FUNCT_4:128;
then A2: B in dom h by ENUMSET1:def 1;
A3: rng h c= {(h . B),(h . C),(h . D)}
proof
let t be object ; :: 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 object such that
A4: x1 in dom h and
A5: t = h . x1 by FUNCT_1:def 3;
now :: thesis: ( ( x1 = D & t in {(h . B),(h . C),(h . D)} ) or ( x1 = B & t in {(h . B),(h . C),(h . D)} ) or ( x1 = C & t in {(h . B),(h . C),(h . D)} ) )
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 object ; :: 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 :: thesis: ( ( t = h . D & t in rng h ) or ( t = h . B & t in rng h ) or ( t = h . C & t in rng h ) )
per cases ( t = h . D or t = h . B or t = h . C ) by A8, ENUMSET1:def 1;
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