let Y be non empty set ; :: thesis: for G being Subset of
for A, B, C, D being a_partition of Y
for h being Function
for A', B', C', D' being set st G = {A,B,C,D} & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D)}
let G be Subset of ; :: thesis: for A, B, C, D being a_partition of Y
for h being Function
for A', B', C', D' being set st G = {A,B,C,D} & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D)}
let A, B, C, D be a_partition of Y; :: thesis: for h being Function
for A', B', C', D' being set st G = {A,B,C,D} & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D)}
let h be Function; :: thesis: for A', B', C', D' being set st G = {A,B,C,D} & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D)}
let A', B', C', D' be set ; :: thesis: ( G = {A,B,C,D} & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') implies rng h = {(h . A),(h . B),(h . C),(h . D)} )
assume that
A1: G = {A,B,C,D} and
A2: h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') ; :: thesis: rng h = {(h . A),(h . B),(h . C),(h . D)}
A3: dom h = G by A1, A2, Th19;
then A4: B in dom h by A1, ENUMSET1:def 2;
A5: rng h c= {(h . A),(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 . A),(h . B),(h . C),(h . D)} )
assume t in rng h ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D)}
then consider x1 being set such that
A6: x1 in dom h and
A7: t = h . x1 by FUNCT_1:def 5;

now

per cases ( x1 = A or x1 = B or x1 = C or x1 = D ) by A1, A3, A6, ENUMSET1:def 2;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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

end;

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

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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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