let A, B, C, D, E be set ; 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; 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 ; ( 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)
; 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
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)} )
assume
t in rng h
;
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 ( ( 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)}
;
verum
end;
A8:
E in dom h
by A1, ENUMSET1:def 3;
A9:
A in dom h
by A1, ENUMSET1:def 3;
{(h . A),(h . B),(h . C),(h . D),(h . E)} c= rng h
hence
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)}
by A5, XBOOLE_0:def 10; verum