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)}
proof
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;
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)} ) )
per cases ( x1 = A or x1 = B or x1 = C or x1 = D or x1 = E or x1 = F ) by A1, A4, ENUMSET1:def 4;
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;
case x1 = E ; :: 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 = F ; :: 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;
end;
end;
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)} ; :: thesis: verum
end;
A6: D in dom h by A1, ENUMSET1:def 4;
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
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
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 ) )
per cases ( t = h . A or t = h . B or t = h . C or t = h . D or t = h . E or t = h . F ) by A11, ENUMSET1:def 4;
end;
end;
hence t in rng h ; :: thesis: verum
end;
hence rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)} by A3, XBOOLE_0:def 10; :: thesis: verum