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 ;
A4: C in dom h by ;
A5: rng h c= {(h . A),(h . B),(h . C),(h . D),(h . E)}
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)} )
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)} ) )
per cases ( x1 = A or x1 = B or x1 = C or x1 = D or x1 = E ) by ;
case x1 = A ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E)} by ; :: thesis: verum
end;
case x1 = B ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E)} by ; :: thesis: verum
end;
case x1 = C ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E)} by ; :: thesis: verum
end;
case x1 = D ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E)} by ; :: thesis: verum
end;
case x1 = E ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E)} by ; :: thesis: verum
end;
end;
end;
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E)} ; :: thesis: verum
end;
A8: E in dom h by ;
A9: A in dom h by ;
{(h . A),(h . B),(h . C),(h . D),(h . E)} 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)} or t in rng h )
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 ) )
per cases ( t = h . A or t = h . B or t = h . C or t = h . D or t = h . E ) by ;
case t = h . A ; :: thesis: t in rng h
hence t in rng h by ; :: thesis: verum
end;
case t = h . B ; :: thesis: t in rng h
hence t in rng h by ; :: thesis: verum
end;
case t = h . C ; :: thesis: t in rng h
hence t in rng h by ; :: thesis: verum
end;
case t = h . D ; :: thesis: t in rng h
hence t in rng h by ; :: thesis: verum
end;
case t = h . E ; :: thesis: t in rng h
hence t in rng h by ; :: thesis: verum
end;
end;
end;
hence t in rng h ; :: thesis: verum
end;
hence rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)} by ; :: thesis: verum