let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y
for h being Function
for A9, B9, C9, D9 being object st G = {A,B,C,D} & h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D)}
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D being a_partition of Y
for h being Function
for A9, B9, C9, D9 being object st G = {A,B,C,D} & h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) 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 A9, B9, C9, D9 being object st G = {A,B,C,D} & h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D)}
let h be Function; :: thesis: for A9, B9, C9, D9 being object st G = {A,B,C,D} & h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D)}
let A9, B9, C9, D9 be object ; :: thesis: ( G = {A,B,C,D} & h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) implies rng h = {(h . A),(h . B),(h . C),(h . D)} )
assume that
A1: G = {A,B,C,D} and
A2: h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) ; :: thesis: rng h = {(h . A),(h . B),(h . C),(h . D)}
A3: dom h = G by A1, A2, Th16;
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 object ; :: 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 object such that
A6: x1 in dom h and
A7: t = h . x1 by FUNCT_1:def 3;

now :: thesis: ( ( x1 = A & t in {(h . A),(h . B),(h . C),(h . D)} ) or ( x1 = B & t in {(h . A),(h . B),(h . C),(h . D)} ) or ( x1 = C & t in {(h . A),(h . B),(h . C),(h . D)} ) or ( x1 = D & t in {(h . A),(h . B),(h . C),(h . D)} ) )

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 object ; :: 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 3; :: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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