let a, b, c, d be set ; ( a <> b implies product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))} )
assume A1:
a <> b
; 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 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 ;
( ( 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 ) ) )
( 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))}
;
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);
( 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;
( 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;
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 ;
( x in dom ((a,b) --> ({c},{d})) implies g . x in ((a,b) --> ({c},{d})) . x )
assume
x in dom ((a,b) --> ({c},{d}))
;
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;
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
;
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;
verum end;
hence
product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))}
by Def5; verum