let a, b, c, x, y, z, w, d be object ; :: thesis: ( x,y,w,z are_mutually_distinct implies rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d} )
set h = (x,y,w,z) --> (a,b,c,d);
assume A1: x,y,w,z are_mutually_distinct ; :: thesis: rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d}
A2: rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d} by Th138;
{a,b,c,d} c= rng ((x,y,w,z) --> (a,b,c,d))

proof

set h = (x,y,w,z) --> (a,b,c,d);
let y1 be object ; :: 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 A3: ( y1 = a or y1 = b or y1 = c or y1 = d ) by ENUMSET1:def 2;
A4: dom ((x,y,w,z) --> (a,b,c,d)) = {x,y,w,z} by Th137;
A5: ( ((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, A3, Th139, Th140, Th141, Th142;
A6: x in dom ((x,y,w,z) --> (a,b,c,d)) by A4, ENUMSET1:def 2;
A7: y in dom ((x,y,w,z) --> (a,b,c,d)) by A4, ENUMSET1:def 2;
A8: w in dom ((x,y,w,z) --> (a,b,c,d)) by A4, ENUMSET1:def 2;
z in dom ((x,y,w,z) --> (a,b,c,d)) by A4, ENUMSET1:def 2;
hence y1 in rng ((x,y,w,z) --> (a,b,c,d)) by A5, A6, A7, A8, FUNCT_1:def 3; :: thesis: verum

end;

hence rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d} by A2; :: thesis: verum