let A, B, C, D, E, F, J, M be set ; :: thesis: for h being Function
for A', B', C', D', E', F', J', M' being set st h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)}
let h be Function; :: thesis: for A', B', C', D', E', F', J', M' being set st h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)}
let A', B', C', D', E', F', J', M' be set ; :: thesis: ( h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') implies rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} )
assume h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') ; :: thesis: rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)}
then A1: dom h = {A,B,C,D,E,F,J,M} by Th66;
then B in dom h by ENUMSET1:def 6;
then A2: h . B in rng h by FUNCT_1:def 5;
M in dom h by A1, ENUMSET1:def 6;
then A3: h . M in rng h by FUNCT_1:def 5;
J in dom h by A1, ENUMSET1:def 6;
then A4: h . J in rng h by FUNCT_1:def 5;
F in dom h by A1, ENUMSET1:def 6;
then A5: h . F in rng h by FUNCT_1:def 5;
E in dom h by A1, ENUMSET1:def 6;
then A6: h . E in rng h by FUNCT_1:def 5;
A7: rng h c= {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)}

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in rng h or t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} )
assume t in rng h ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)}
then consider x1 being set such that
A8: x1 in dom h and
A9: t = h . x1 by FUNCT_1:def 5;
( x1 = A or x1 = B or x1 = C or x1 = D or x1 = E or x1 = F or x1 = J or x1 = M ) by A1, A8, ENUMSET1:def 6;
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} by A9, ENUMSET1:def 6; :: thesis: verum

end;

D in dom h by A1, ENUMSET1:def 6;
then A10: h . D in rng h by FUNCT_1:def 5;
C in dom h by A1, ENUMSET1:def 6;
then A11: h . C in rng h by FUNCT_1:def 5;
A in dom h by A1, ENUMSET1:def 6;
then A12: h . A in rng h by FUNCT_1:def 5;
{(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} c= rng h

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} or t in rng h )
assume t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} ; :: thesis: t in rng h
hence t in rng h by A12, A2, A11, A10, A6, A5, A4, A3, ENUMSET1:def 6; :: thesis: verum

end;

hence rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} by A7, XBOOLE_0:def 10; :: thesis: verum