let A, B, C, D, E be set ; :: thesis: for h being Function

for A9, B9, C9, D9, E9 being set st h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds

rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)}

let h be Function; :: thesis: for A9, B9, C9, D9, E9 being set st h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds

rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)}

let A9, B9, C9, D9, E9 be set ; :: thesis: ( h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) implies rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)} )

assume h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) ; :: thesis: rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)}

then A1: dom h = {A,B,C,D,E} by Th27;

then A2: B in dom h by ENUMSET1:def 3;

A3: D in dom h by A1, ENUMSET1:def 3;

A4: C in dom h by A1, ENUMSET1:def 3;

A5: rng h c= {(h . A),(h . B),(h . C),(h . D),(h . E)}

A9: A in dom h by A1, ENUMSET1:def 3;

{(h . A),(h . B),(h . C),(h . D),(h . E)} c= rng h

for A9, B9, C9, D9, E9 being set st h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds

rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)}

let h be Function; :: thesis: for A9, B9, C9, D9, E9 being set st h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds

rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)}

let A9, B9, C9, D9, E9 be set ; :: thesis: ( h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) implies rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)} )

assume h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) ; :: thesis: rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)}

then A1: dom h = {A,B,C,D,E} by Th27;

then A2: B in dom h by ENUMSET1:def 3;

A3: D in dom h by A1, ENUMSET1:def 3;

A4: C in dom h by A1, ENUMSET1:def 3;

A5: rng h c= {(h . A),(h . B),(h . C),(h . D),(h . E)}

proof

A8:
E in dom h
by A1, ENUMSET1:def 3;
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),(h . E)} )

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

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),(h . E)}

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),(h . E)} ) or ( x1 = B & t in {(h . A),(h . B),(h . C),(h . D),(h . E)} ) or ( x1 = C & t in {(h . A),(h . B),(h . C),(h . D),(h . E)} ) or ( x1 = D & t in {(h . A),(h . B),(h . C),(h . D),(h . E)} ) or ( x1 = E & t in {(h . A),(h . B),(h . C),(h . D),(h . E)} ) )end;

hence
t in {(h . A),(h . B),(h . C),(h . D),(h . E)}
; :: thesis: verumper cases
( x1 = A or x1 = B or x1 = C or x1 = D or x1 = E )
by A1, A6, ENUMSET1:def 3;

end;

A9: A in dom h by A1, ENUMSET1:def 3;

{(h . A),(h . B),(h . C),(h . D),(h . E)} c= rng h

proof

hence
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)}
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),(h . E)} or t in rng h )

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

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

now :: thesis: ( ( t = h . A & t in rng h ) or ( t = h . B & t in rng h ) or ( t = h . C & t in rng h ) or ( t = h . D & t in rng h ) or ( t = h . E & t in rng h ) )

hence
t in rng h
; :: thesis: verumend;