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