let a, b, x, y, z be set ; :: thesis: for c being complex number st a,b,c are_mutually_different holds
product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))}
let c be complex number ; :: thesis: ( a,b,c are_mutually_different implies product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))} )
assume A1: a,b,c are_mutually_different ; :: thesis: product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))}
set X = {((a,b,c) --> (x,y,z))};
set f = (a,b,c) --> ({x},{y},{z});
A2: dom ((a,b,c) --> ({x},{y},{z})) = {a,b,c} by BVFUNC14:11;

now :: thesis: for m being set holds
( ( m in {((a,b,c) --> (x,y,z))} implies ex g being Function st
( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) ) & ( ex g being Function st
( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) implies m in {((a,b,c) --> (x,y,z))} ) )

let m be set ; :: thesis: ( ( m in {((a,b,c) --> (x,y,z))} implies ex g being Function st
( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) ) & ( ex g being Function st
( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) implies m in {((a,b,c) --> (x,y,z))} ) )
thus ( m in {((a,b,c) --> (x,y,z))} implies ex g being Function st
( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) ) :: thesis: ( ex g being Function st
( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) implies m in {((a,b,c) --> (x,y,z))} )

proof

assume A3: m in {((a,b,c) --> (x,y,z))} ; :: thesis: ex g being Function st
( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) )
take g = (a,b,c) --> (x,y,z); :: thesis: ( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) )
thus m = g by A3, TARSKI:def 1; :: thesis: ( dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) )
thus dom g = dom ((a,b,c) --> ({x},{y},{z})) by A2, BVFUNC14:11; :: thesis: for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x
let k be set ; :: thesis: ( k in dom ((a,b,c) --> ({x},{y},{z})) implies g . k in ((a,b,c) --> ({x},{y},{z})) . k )
assume k in dom ((a,b,c) --> ({x},{y},{z})) ; :: thesis: g . k in ((a,b,c) --> ({x},{y},{z})) . k
then A4: ( k = a or k = b or k = c ) by A2, ENUMSET1:def 1;
( g . a = x & ((a,b,c) --> ({x},{y},{z})) . a = {x} & g . b = y & ((a,b,c) --> ({x},{y},{z})) . b = {y} & g . c = z & ((a,b,c) --> ({x},{y},{z})) . c = {z} ) by A1, Th28;
hence g . k in ((a,b,c) --> ({x},{y},{z})) . k by A4, TARSKI:def 1; :: thesis: verum

end;

given g being Function such that A5: m = g and
A6: dom g = dom ((a,b,c) --> ({x},{y},{z})) and
A7: for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ; :: thesis: m in {((a,b,c) --> (x,y,z))}
( a in dom ((a,b,c) --> ({x},{y},{z})) & b in dom ((a,b,c) --> ({x},{y},{z})) & c in dom ((a,b,c) --> ({x},{y},{z})) ) by A2, ENUMSET1:def 1;
then ( g . a in ((a,b,c) --> ({x},{y},{z})) . a & g . b in ((a,b,c) --> ({x},{y},{z})) . b & g . c in ((a,b,c) --> ({x},{y},{z})) . c & ((a,b,c) --> ({x},{y},{z})) . a = {x} & ((a,b,c) --> ({x},{y},{z})) . b = {y} & ((a,b,c) --> ({x},{y},{z})) . c = {z} ) by A1, A7, Th28;
then ( g . a = x & g . b = y & g . c = z ) by TARSKI:def 1;
then g = (a,b,c) --> (x,y,z) by A2, A6, Th29;
hence m in {((a,b,c) --> (x,y,z))} by A5, TARSKI:def 1; :: thesis: verum

end;

hence product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))} by CARD_3:def 5; :: thesis: verum