let x, y, w, z, a, b, c, d be set ; :: thesis: ( x,y,w,z are_mutually_different 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_different ; :: 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 Th2;
{a,b,c,d} c= rng ((x,y,w,z) --> (a,b,c,d)) by A1, Lm2;
hence rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d} by A2, XBOOLE_0:def 10; :: thesis: verum