let A, B, C, D, E, F be set ; :: thesis: for h being Function
for A', B', C', D', E', F' being set st h = (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)}
let h be Function; :: thesis: for A', B', C', D', E', F' being set st h = (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)}
let A', B', C', D', E', F' be set ; :: thesis: ( h = (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') implies rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)} )
assume h = (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') ; :: thesis: rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)}
then A1: dom h = {A,B,C,D,E,F} by Th41;
then A2: B in dom h by ENUMSET1:def 4;
A3: rng h c= {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)}

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)} )
assume t in rng h ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)}
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 = A or x1 = B or x1 = C or x1 = D or x1 = E or x1 = F ) by A1, A4, ENUMSET1:def 4;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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

end;

A6: D in dom h by A1, ENUMSET1:def 4;
A7: C in dom h by A1, ENUMSET1:def 4;
A8: F in dom h by A1, ENUMSET1:def 4;
A9: E in dom h by A1, ENUMSET1:def 4;
A10: A in dom h by A1, ENUMSET1:def 4;
{(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)} 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)} or t in rng h )
assume A11: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)} ; :: thesis: t in rng h

now

per cases ( t = h . A or t = h . B or t = h . C or t = h . D or t = h . E or t = h . F ) by A11, ENUMSET1:def 4;

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

hence t in rng h by A10, 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 A7, FUNCT_1:def 5; :: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

hence t in rng h ; :: thesis: verum

end;

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