let x, y, w, z, a, b, c, d be set ; :: thesis: ( x,y,w,z are_mutually_different implies {a,b,c,d} c= rng (x,y,w,z --> a,b,c,d) )
set h = x,y,w,z --> a,b,c,d;
assume A1: x,y,w,z are_mutually_different ; :: thesis: {a,b,c,d} c= rng (x,y,w,z --> a,b,c,d)
let y1 be set ; :: according to TARSKI:def 3 :: thesis: ( not y1 in {a,b,c,d} or y1 in rng (x,y,w,z --> a,b,c,d) )
assume y1 in {a,b,c,d} ; :: thesis: y1 in rng (x,y,w,z --> a,b,c,d)
then A2: ( y1 = a or y1 = b or y1 = c or y1 = d ) by ENUMSET1:def 2;
A3: dom (x,y,w,z --> a,b,c,d) = {x,y,w,z} by Th1;
A4: ( (x,y,w,z --> a,b,c,d) . x = y1 or (x,y,w,z --> a,b,c,d) . y = y1 or (x,y,w,z --> a,b,c,d) . w = y1 or (x,y,w,z --> a,b,c,d) . z = y1 ) by A1, A2, Th3;
A5: x in dom (x,y,w,z --> a,b,c,d) by A3, ENUMSET1:def 2;
A6: y in dom (x,y,w,z --> a,b,c,d) by A3, ENUMSET1:def 2;
A7: w in dom (x,y,w,z --> a,b,c,d) by A3, ENUMSET1:def 2;
z in dom (x,y,w,z --> a,b,c,d) by A3, ENUMSET1:def 2;
hence y1 in rng (x,y,w,z --> a,b,c,d) by A4, A5, A6, A7, FUNCT_1:def 5; :: thesis: verum