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 3; :: thesis: verum