let a, b, c, x, y, z, w, d be object ; ( 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
; 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 ;
TARSKI:def 3 ( 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}
;
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;
verum
end;
hence
rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d}
by A2; verum