let A be set ; for x being object holds
( x in 2 -tuples_on A iff ex a, b being object st
( a in A & b in A & x = <*a,b*> ) )
let x be object ; ( x in 2 -tuples_on A iff ex a, b being object st
( a in A & b in A & x = <*a,b*> ) )
hereby ( ex a, b being object st
( a in A & b in A & x = <*a,b*> ) implies x in 2 -tuples_on A )
assume
x in 2
-tuples_on A
;
ex a, b being object st
( a in A & b in A & x = <*a,b*> )then
x in { s where s is Element of A * : len s = 2 }
;
then consider s being
Element of
A * such that A1:
x = s
and A2:
len s = 2
;
reconsider a =
s . 1,
b =
s . 2 as
object ;
take a =
a;
ex b being object st
( a in A & b in A & x = <*a,b*> )take b =
b;
( a in A & b in A & x = <*a,b*> )A3:
(
rng <*a,b*> = {a,b} &
a in {a,b} )
by Lm1, TARSKI:def 2;
A4:
(
b in {a,b} &
rng s c= A )
by RELAT_1:def 19, TARSKI:def 2;
x = <*a,b*>
by A1, A2, FINSEQ_1:44;
hence
(
a in A &
b in A &
x = <*a,b*> )
by A1, A3, A4;
verum
end;
given a, b being object such that A5:
a in A
and
A6:
b in A
and
A7:
x = <*a,b*>
; x in 2 -tuples_on A
reconsider A = A as non empty set by A5;
reconsider a = a, b = b as Element of A by A5, A6;
<*a,b*> is Element of 2 -tuples_on A
by Th99;
hence
x in 2 -tuples_on A
by A7; verum