let a, b, c, d be set ; :: thesis: ( a <> b implies product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))} )
assume A1: a <> b ; :: thesis: product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))}
set X = {((a,b) --> (c,d))};
set f = (a,b) --> ({c},{d});
A2: dom ((a,b) --> ({c},{d})) = {a,b} by FUNCT_4:62;

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

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

proof

assume A3: x in {((a,b) --> (c,d))} ; :: thesis: ex g being Function st
( x = g & dom g = dom ((a,b) --> ({c},{d})) & ( for x being object st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x ) )
take g = (a,b) --> (c,d); :: thesis: ( x = g & dom g = dom ((a,b) --> ({c},{d})) & ( for x being object st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x ) )
thus x = g by A3, TARSKI:def 1; :: thesis: ( dom g = dom ((a,b) --> ({c},{d})) & ( for x being object st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x ) )
thus dom g = dom ((a,b) --> ({c},{d})) by A2, FUNCT_4:62; :: thesis: for x being object st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x
let x be object ; :: thesis: ( x in dom ((a,b) --> ({c},{d})) implies g . x in ((a,b) --> ({c},{d})) . x )
assume x in dom ((a,b) --> ({c},{d})) ; :: thesis: g . x in ((a,b) --> ({c},{d})) . x
then A4: ( x = a or x = b ) by A2, TARSKI:def 2;
A5: g . a = c by A1, FUNCT_4:63;
A6: ((a,b) --> ({c},{d})) . a = {c} by A1, FUNCT_4:63;
A7: g . b = d by FUNCT_4:63;
((a,b) --> ({c},{d})) . b = {d} by FUNCT_4:63;
hence g . x in ((a,b) --> ({c},{d})) . x by A4, A5, A6, A7, TARSKI:def 1; :: thesis: verum

end;

given g being Function such that A8: x = g and
A9: dom g = dom ((a,b) --> ({c},{d})) and
A10: for x being object st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x ; :: thesis: x in {((a,b) --> (c,d))}
A11: a in dom ((a,b) --> ({c},{d})) by A2, TARSKI:def 2;
A12: b in dom ((a,b) --> ({c},{d})) by A2, TARSKI:def 2;
A13: g . a in ((a,b) --> ({c},{d})) . a by A10, A11;
A14: g . b in ((a,b) --> ({c},{d})) . b by A10, A12;
A15: ((a,b) --> ({c},{d})) . a = {c} by A1, FUNCT_4:63;
A16: ((a,b) --> ({c},{d})) . b = {d} by FUNCT_4:63;
A17: g . a = c by A13, A15, TARSKI:def 1;
g . b = d by A14, A16, TARSKI:def 1;
then g = (a,b) --> (c,d) by A2, A9, A17, FUNCT_4:66;
hence x in {((a,b) --> (c,d))} by A8, TARSKI:def 1; :: thesis: verum

end;

hence product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))} by Def5; :: thesis: verum