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

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

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

A8:
D in dom h
by A1, A3, ENUMSET1:def 2;
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;

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

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

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

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

end;assume A11: t in {(h . A),(h . B),(h . C),(h . D)} ; :: thesis: t in rng h