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

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

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

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

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

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

assume h = (((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (A .--> A9) ; :: 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 Th38;

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

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

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

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

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

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

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

assume h = (((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (A .--> A9) ; :: 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 Th38;

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

A6:
D in dom h
by A1, ENUMSET1:def 4;
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),(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 object such that

A4: x1 in dom h and

A5: 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),(h . F)}

then consider x1 being object such that

A4: x1 in dom h and

A5: t = h . x1 by FUNCT_1:def 3;

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

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

end;

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;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

hence
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)}
by A3, 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),(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

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

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