let a, b, c, x, y, z be object ; :: thesis: ( a,b,c are_mutually_distinct implies product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))} )
assume A1: a,b,c are_mutually_distinct ; :: 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 FUNCT_4:128;
now :: thesis: for m being object 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 object 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 object 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 object ; :: 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 object 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 object 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 object 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 object 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 object 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 object 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 object 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, FUNCT_4:128; :: thesis: for x being object st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x
let k be object ; :: 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, FUNCT_4:135, FUNCT_4:134;
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 object 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, FUNCT_4:135, FUNCT_4:134;
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, FUNCT_4:136;
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