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;
A5: g . a = c by A1, FUNCT_4:66;
A6: (a,b --> {c},{d}) . a = {c} by A1, FUNCT_4:66;
A7: g . b = d by FUNCT_4:66;
(a,b --> {c},{d}) . b = {d} by FUNCT_4:66;
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 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)}
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:66;
A16: (a,b --> {c},{d}) . b = {d} by FUNCT_4:66;
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:69;
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