let A, B, C, D, E, F, J be set ; for h being Function
for A9, B9, C9, D9, E9, F9, J9 being set st h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
let h be Function; for A9, B9, C9, D9, E9, F9, J9 being set st h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
let A9, B9, C9, D9, E9, F9, J9 be set ; ( h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) implies rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)} )
assume
h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9)
; rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
then A1:
dom h = {A,B,C,D,E,F,J}
by Th50;
then
B in dom h
by ENUMSET1:def 5;
then A2:
h . B in rng h
by FUNCT_1:def 3;
F in dom h
by A1, ENUMSET1:def 5;
then A3:
h . F in rng h
by FUNCT_1:def 3;
E in dom h
by A1, ENUMSET1:def 5;
then A4:
h . E in rng h
by FUNCT_1:def 3;
D in dom h
by A1, ENUMSET1:def 5;
then A5:
h . D in rng h
by FUNCT_1:def 3;
C in dom h
by A1, ENUMSET1:def 5;
then A6:
h . C in rng h
by FUNCT_1:def 3;
J in dom h
by A1, ENUMSET1:def 5;
then A7:
h . J in rng h
by FUNCT_1:def 3;
A8:
rng h c= {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
proof
let t be
object ;
TARSKI:def 3 ( not t in rng h or t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)} )
assume
t in rng h
;
t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
then consider x1 being
object such that A9:
x1 in dom h
and A10:
t = h . x1
by FUNCT_1:def 3;
(
x1 = A or
x1 = B or
x1 = C or
x1 = D or
x1 = E or
x1 = F or
x1 = J )
by A1, A9, ENUMSET1:def 5;
hence
t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
by A10, ENUMSET1:def 5;
verum
end;
A in dom h
by A1, ENUMSET1:def 5;
then A11:
h . A in rng h
by FUNCT_1:def 3;
{(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)} c= rng h
by A11, A2, A6, A5, A4, A3, A7, ENUMSET1:def 5;
hence
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
by A8, XBOOLE_0:def 10; verum