let a1, a2, a3, b1, b2, b3 be object ; :: thesis: ( a1,a2,a3 are_mutually_distinct implies rng ((a1,a2,a3) --> (b1,b2,b3)) = {b1,b2,b3} )
assume A1: a1,a2,a3 are_mutually_distinct ; :: thesis: rng ((a1,a2,a3) --> (b1,b2,b3)) = {b1,b2,b3}
set f = (a1,a2,a3) --> (b1,b2,b3);
thus rng ((a1,a2,a3) --> (b1,b2,b3)) c= {b1,b2,b3} :: according to XBOOLE_0:def 10 :: thesis: {b1,b2,b3} c= rng ((a1,a2,a3) --> (b1,b2,b3))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((a1,a2,a3) --> (b1,b2,b3)) or x in {b1,b2,b3} )
assume x in rng ((a1,a2,a3) --> (b1,b2,b3)) ; :: thesis: x in {b1,b2,b3}
then consider y being object such that
A2: ( y in dom ((a1,a2,a3) --> (b1,b2,b3)) & x = ((a1,a2,a3) --> (b1,b2,b3)) . y ) by FUNCT_1:def 3;
dom ((a1,a2,a3) --> (b1,b2,b3)) = {a1,a2,a3} by Th128;
then ( y = a1 or y = a2 or y = a3 ) by A2, ENUMSET1:def 1;
then ( x = b1 or x = b2 or x = b3 ) by A2, A1, Th134, Th135;
hence x in {b1,b2,b3} by ENUMSET1:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {b1,b2,b3} or x in rng ((a1,a2,a3) --> (b1,b2,b3)) )
assume x in {b1,b2,b3} ; :: thesis: x in rng ((a1,a2,a3) --> (b1,b2,b3))
then A3: ( x = b1 or x = b2 or x = b3 ) by ENUMSET1:def 1;
A4: ( a1 in {a1,a2,a3} & a2 in {a1,a2,a3} & a3 in {a1,a2,a3} ) by ENUMSET1:def 1;
A5: dom ((a1,a2,a3) --> (b1,b2,b3)) = {a1,a2,a3} by Th128;
( ((a1,a2,a3) --> (b1,b2,b3)) . a1 = b1 & ((a1,a2,a3) --> (b1,b2,b3)) . a2 = b2 & ((a1,a2,a3) --> (b1,b2,b3)) . a3 = b3 ) by A1, Th134, Th135;
hence x in rng ((a1,a2,a3) --> (b1,b2,b3)) by A3, A4, A5, FUNCT_1:def 3; :: thesis: verum