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)}

A7: D in dom h by A1, ENUMSET1:def 1;

{(h . B),(h . C),(h . D)} c= rng h

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

A6:
C in dom h
by A1, ENUMSET1:def 1;
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;

end;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)} ) )

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

A7: D in dom h by A1, ENUMSET1:def 1;

{(h . B),(h . C),(h . D)} c= rng h

proof

hence
rng h = {(h . B),(h . C),(h . D)}
by A3, XBOOLE_0:def 10; :: thesis: verum
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

end;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 ) )end;

hence
t in rng h
; :: thesis: verum