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:65;

now

let x be set ; :: 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 set 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 set 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 set 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 set 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 set 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 set 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 set 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:65; :: thesis: for x being set st x in dom (a,b --> {c},{d}) holds
g . x in (a,b --> {c},{d}) . x
let x be set ; :: 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;
( g . a = c & (a,b --> {c},{d}) . a = {c} & g . b = d & (a,b --> {c},{d}) . b = {d} ) by A1, FUNCT_4:66;
hence g . x in (a,b --> {c},{d}) . x by A4, TARSKI:def 1; :: thesis: verum

end;

given g being Function such that A5: x = g and
A6: dom g = dom (a,b --> {c},{d}) and
A7: for x being set st x in dom (a,b --> {c},{d}) holds
g . x in (a,b --> {c},{d}) . x ; :: thesis: x in {(a,b --> c,d)}
( a in dom (a,b --> {c},{d}) & b in dom (a,b --> {c},{d}) ) by A2, TARSKI:def 2;
then ( g . a in (a,b --> {c},{d}) . a & g . b in (a,b --> {c},{d}) . b & (a,b --> {c},{d}) . a = {c} & (a,b --> {c},{d}) . b = {d} ) by A1, A7, FUNCT_4:66;
then ( g . a = c & g . b = d ) by TARSKI:def 1;
then g = a,b --> c,d by A2, A6, FUNCT_4:69;
hence x in {(a,b --> c,d)} by A5, TARSKI:def 1; :: thesis: verum

end;

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