let A, B, C, D, E, F, J, M, N be set ; :: thesis: for h being Function
for A9, B9, C9, D9, E9, F9, J9, M9, N9 being set st h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
let h be Function; :: thesis: for A9, B9, C9, D9, E9, F9, J9, M9, N9 being set st h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
let A9, B9, C9, D9, E9, F9, J9, M9, N9 be set ; :: thesis: ( h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) implies rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} )
assume h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) ; :: thesis: rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
then A1: dom h = {A,B,C,D,E,F,J,M,N} by Th77;
then A2: B in dom h by ENUMSET1:def 7;
A3: M in dom h by A1, ENUMSET1:def 7;
A4: J in dom h by A1, ENUMSET1:def 7;
A5: N in dom h by A1, ENUMSET1:def 7;
A6: D in dom h by A1, ENUMSET1:def 7;
A7: C in dom h by A1, ENUMSET1:def 7;
A8: rng h c= {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
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),(h . J),(h . M),(h . N)} )
assume t in rng h ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
then consider x1 being object such that
A9: x1 in dom h and
A10: 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),(h . J),(h . M),(h . N)} ) or ( x1 = B & t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} ) or ( x1 = C & t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} ) or ( x1 = D & t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} ) or ( x1 = E & t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} ) or ( x1 = F & t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} ) or ( x1 = J & t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} ) or ( x1 = M & t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} ) or ( x1 = N & t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} ) )
per cases ( x1 = A or x1 = B or x1 = C or x1 = D or x1 = E or x1 = F or x1 = J or x1 = M or x1 = N ) by A1, A9, ENUMSET1:def 7;
case x1 = A ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} by A10, ENUMSET1:def 7; :: thesis: verum
end;
case x1 = B ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} by A10, ENUMSET1:def 7; :: thesis: verum
end;
case x1 = C ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} by A10, ENUMSET1:def 7; :: thesis: verum
end;
case x1 = D ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} by A10, ENUMSET1:def 7; :: thesis: verum
end;
case x1 = E ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} by A10, ENUMSET1:def 7; :: thesis: verum
end;
case x1 = F ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} by A10, ENUMSET1:def 7; :: thesis: verum
end;
case x1 = J ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} by A10, ENUMSET1:def 7; :: thesis: verum
end;
case x1 = M ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} by A10, ENUMSET1:def 7; :: thesis: verum
end;
case x1 = N ; :: thesis: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} by A10, ENUMSET1:def 7; :: thesis: verum
end;
end;
end;
hence t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} ; :: thesis: verum
end;
A11: F in dom h by A1, ENUMSET1:def 7;
A12: E in dom h by A1, ENUMSET1:def 7;
A13: A in dom h by A1, ENUMSET1:def 7;
{(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} 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),(h . J),(h . M),(h . N)} or t in rng h )
assume A14: t in {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} ; :: 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 ) or ( t = h . J & t in rng h ) or ( t = h . M & t in rng h ) or ( t = h . N & 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 or t = h . J or t = h . M or t = h . N ) by A14, ENUMSET1:def 7;
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),(h . J),(h . M),(h . N)} by A8, XBOOLE_0:def 10; :: thesis: verum